author  blanchet 
Sun, 01 May 2011 18:37:25 +0200  
changeset 42570  77f94ac04f32 
parent 42569  5737947e4c77 
child 42572  0c9a947b43fc 
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 = 
42523
08346ea46a59
added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents:
42522
diff
changeset

16 
Many_Typed  
42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42547
diff
changeset

17 
Mangled of bool  
42523
08346ea46a59
added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents:
42522
diff
changeset

18 
Args of bool  
42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42547
diff
changeset

19 
Tags of bool  
41134  20 
No_Types 
21 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

22 
val readable_names : 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 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

25 
val predicator_base : string 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

26 
val explicit_app_base : string 
42549
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42548
diff
changeset

27 
val type_pred_base : string 
42562  28 
val tff_type_prefix : string 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

29 
val is_type_system_sound : type_system > bool 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

30 
val type_system_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

31 
val num_atp_type_args : theory > type_system > string > int 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

32 
val unmangled_const : string > string * string fo_term list 
41088  33 
val translate_atp_fact : 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

34 
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

35 
> translated_formula option * ((string * 'a) * thm) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39975
diff
changeset

36 
val prepare_atp_problem : 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

37 
Proof.context > 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

38 
> (translated_formula option * ((string * 'a) * thm)) list 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42540
diff
changeset

39 
> string problem * string Symtab.table * int * int 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42540
diff
changeset

40 
* (string * 'a) list vector 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

41 
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

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

43 

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

44 
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

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

46 

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

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

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

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

50 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

51 
(* Readable names are often much shorter, especially if types are mangled in 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

52 
names. For that reason, they are on by default. *) 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

53 
val readable_names = Unsynchronized.ref true 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

54 

42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

55 
val type_decl_prefix = "type_" 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

56 
val sym_decl_prefix = "sym_" 
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

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

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

59 
val helper_prefix = "help_" 
42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

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

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

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

63 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

64 
val predicator_base = "hBOOL" 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

65 
val explicit_app_base = "hAPP" 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

66 
val type_pred_base = "is" 
42562  67 
val tff_type_prefix = "ty_" 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

68 

42562  69 
fun make_tff_type s = tff_type_prefix ^ ascii_of s 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

70 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

71 
(* official TPTP syntax *) 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

72 
val tptp_tff_type_of_types = "$tType" 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

73 
val tptp_tff_bool_type = "$o" 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

74 
val tptp_false = "$false" 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

75 
val tptp_true = "$true" 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

76 

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

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

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

79 

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

81 
{name: string, 
42525
7a506b0b644f
distinguish FOF and TFF (typed firstorder) in ATP abstract syntax tree
blanchet
parents:
42524
diff
changeset

82 
kind: formula_kind, 
42562  83 
combformula: (name, typ, combterm) formula, 
84 
atomic_types: typ list} 

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

85 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

86 
fun update_combformula f 
42562  87 
({name, kind, combformula, atomic_types} : translated_formula) = 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

88 
{name = name, kind = kind, combformula = f combformula, 
42562  89 
atomic_types = atomic_types} : translated_formula 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

90 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

91 
fun fact_lift f ({combformula, ...} : translated_formula) = f combformula 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

92 

41134  93 
datatype type_system = 
42523
08346ea46a59
added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents:
42522
diff
changeset

94 
Many_Typed  
42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42547
diff
changeset

95 
Mangled of bool  
42523
08346ea46a59
added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents:
42522
diff
changeset

96 
Args of bool  
42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42547
diff
changeset

97 
Tags of bool  
41134  98 
No_Types 
99 

42523
08346ea46a59
added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents:
42522
diff
changeset

100 
fun is_type_system_sound Many_Typed = true 
42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42547
diff
changeset

101 
 is_type_system_sound (Mangled full_types) = full_types 
42523
08346ea46a59
added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents:
42522
diff
changeset

102 
 is_type_system_sound (Args full_types) = full_types 
42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42547
diff
changeset

103 
 is_type_system_sound (Tags full_types) = full_types 
42523
08346ea46a59
added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents:
42522
diff
changeset

104 
 is_type_system_sound No_Types = false 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

105 

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

106 
fun type_system_types_dangerous_types (Tags _) = true 
42523
08346ea46a59
added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents:
42522
diff
changeset

107 
 type_system_types_dangerous_types type_sys = is_type_system_sound type_sys 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

108 

42524  109 
fun dont_need_type_args type_sys s = 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

110 
s <> type_pred_base andalso 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

111 
(member (op =) [@{const_name HOL.eq}] s orelse 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

112 
case type_sys of 
42533  113 
Many_Typed => false 
42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42547
diff
changeset

114 
 Mangled _ => false 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

115 
 Args _ => s = explicit_app_base 
42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42547
diff
changeset

116 
 Tags full_types => full_types orelse s = explicit_app_base 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

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

118 

42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42547
diff
changeset

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

120 

42563  121 
fun general_type_arg_policy Many_Typed = Mangled_Types 
122 
 general_type_arg_policy (Mangled _) = Mangled_Types 

123 
 general_type_arg_policy _ = Explicit_Type_Args 

124 

42524  125 
fun type_arg_policy type_sys s = 
42563  126 
if dont_need_type_args type_sys s then No_Type_Args 
127 
else general_type_arg_policy type_sys 

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

128 

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

129 
fun num_atp_type_args thy type_sys s = 
42557
ae0deb39a254
fixed minarity computation when "explicit_apply" is specified
blanchet
parents:
42556
diff
changeset

130 
if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s 
ae0deb39a254
fixed minarity computation when "explicit_apply" is specified
blanchet
parents:
42556
diff
changeset

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

132 

42353
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

133 
fun atp_type_literals_for_types type_sys kind Ts = 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

134 
if type_sys = No_Types then 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

135 
[] 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

136 
else 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

137 
Ts > type_literals_for_types 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

138 
> filter (fn TyLitVar _ => kind <> Conjecture 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

139 
 TyLitFree _ => kind = Conjecture) 
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

140 

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

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

142 
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

143 
fun mk_aconns c phis = 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

144 
let val (phis', phi') = split_last phis in 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

145 
fold_rev (mk_aconn c) phis' phi' 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

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

147 
fun mk_ahorn [] phi = phi 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

148 
 mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi]) 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

149 
fun mk_aquant _ [] phi = phi 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

150 
 mk_aquant q xs (phi as AQuant (q', xs', phi')) = 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

151 
if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi) 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

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

153 

42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

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

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

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

158 
 formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

159 
 formula_vars bounds (AAtom tm) = 
42526  160 
union (op =) (atom_vars tm [] 
161 
> filter_out (member (op =) bounds o fst)) 

42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

162 
in mk_aquant AForall (formula_vars [] phi []) phi end 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

163 

42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

164 
fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2] 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

165 
 combterm_vars (CombConst _) = I 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

166 
 combterm_vars (CombVar (name, ty)) = insert (op =) (name, SOME ty) 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

167 
val close_combformula_universally = close_universally combterm_vars 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

168 

413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

169 
fun term_vars (ATerm (name as (s, _), tms)) = 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

170 
is_atp_variable s ? insert (op =) (name, NONE) 
42526  171 
#> fold term_vars tms 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

172 
val close_formula_universally = close_universally term_vars 
41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

173 

42562  174 
fun fo_term_from_typ (Type (s, Ts)) = 
175 
ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts) 

176 
 fo_term_from_typ (TFree (s, _)) = 

177 
ATerm (`make_fixed_type_var s, []) 

178 
 fo_term_from_typ (TVar ((x as (s, _)), _)) = 

179 
ATerm ((make_schematic_type_var x, s), []) 

180 

181 
(* This shouldn't clash with anything else. *) 

42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

182 
val mangled_type_sep = "\000" 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

183 

42562  184 
fun generic_mangled_type_name f (ATerm (name, [])) = f name 
185 
 generic_mangled_type_name f (ATerm (name, tys)) = 

186 
f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")" 

187 
val mangled_type_name = 

188 
fo_term_from_typ 

189 
#> (fn ty => (make_tff_type (generic_mangled_type_name fst ty), 

190 
generic_mangled_type_name snd ty)) 

42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

191 

42562  192 
fun generic_mangled_type_suffix f g tys = 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

193 
fold_rev (curry (op ^) o g o prefix mangled_type_sep 
42562  194 
o generic_mangled_type_name f) tys "" 
195 
fun mangled_const_name T_args (s, s') = 

196 
let val ty_args = map fo_term_from_typ T_args in 

197 
(s ^ generic_mangled_type_suffix fst ascii_of ty_args, 

198 
s' ^ generic_mangled_type_suffix snd I ty_args) 

199 
end 

42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

200 

024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

201 
val parse_mangled_ident = 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

202 
Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

203 

024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

204 
fun parse_mangled_type x = 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

205 
(parse_mangled_ident 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

206 
 Scan.optional ($$ "("  Scan.optional parse_mangled_types []  $$ ")") 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

207 
[] >> ATerm) x 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

208 
and parse_mangled_types x = 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

209 
(parse_mangled_type ::: Scan.repeat ($$ ","  parse_mangled_type)) x 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

210 

024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

211 
fun unmangled_type s = 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

212 
s > suffix ")" > raw_explode 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

213 
> Scan.finite Symbol.stopper 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

214 
(Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^ 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

215 
quote s)) parse_mangled_type)) 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

216 
> fst 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

217 

42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

218 
val unmangled_const_name = space_explode mangled_type_sep #> hd 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

219 
fun unmangled_const s = 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

220 
let val ss = space_explode mangled_type_sep s in 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

221 
(hd ss, map unmangled_type (tl ss)) 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

222 
end 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

223 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

224 
val introduce_proxies = 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

225 
let 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

226 
fun aux top_level (CombApp (tm1, tm2)) = 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

227 
CombApp (aux top_level tm1, aux false tm2) 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

228 
 aux top_level (CombConst (name as (s, s'), ty, ty_args)) = 
42570
77f94ac04f32
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents:
42569
diff
changeset

229 
(case proxify_const s of 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

230 
SOME proxy_base => 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

231 
if top_level then 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

232 
(case s of 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

233 
"c_False" => (tptp_false, s') 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

234 
 "c_True" => (tptp_true, s') 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

235 
 _ => name, []) 
42569
5737947e4c77
make sure that fequal keeps its type arguments for mangled type systems
blanchet
parents:
42568
diff
changeset

236 
else 
5737947e4c77
make sure that fequal keeps its type arguments for mangled type systems
blanchet
parents:
42568
diff
changeset

237 
(proxy_base >> prefix const_prefix, ty_args) 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

238 
 NONE => (name, ty_args)) 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

239 
> (fn (name, ty_args) => CombConst (name, ty, ty_args)) 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

240 
 aux _ tm = tm 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

241 
in aux true end 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

242 

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

244 
let 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

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

246 
combterm_from_term thy bs (Envir.eta_contract t) 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

247 
>> (introduce_proxies #> AAtom) 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

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

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

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

251 
do_formula ((s, T) :: bs) t' 
42562  252 
#>> mk_aquant q [(`make_bound_var s, SOME T)] 
38518
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

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

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

255 
do_formula bs t1 ##>> do_formula bs t2 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

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

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

258 
case t of 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

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

260 
 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

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

262 
 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

263 
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

264 
 @{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

265 
 @{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

266 
 @{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

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

268 
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

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

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

271 

38618  272 
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

273 

41491  274 
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

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

276 
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

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

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

279 
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

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

281 

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

282 
(* Removes the lambdas from an equation of the form "t = (%x. u)". 
39890  283 
(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

284 
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

285 
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

286 
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

287 
 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

288 
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

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

290 
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

291 
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

292 
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

293 
$ 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

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

295 
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

296 
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

297 
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

298 
 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

299 
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

300 

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

301 
fun introduce_combinators_in_term ctxt kind t = 
42361  302 
let val thy = Proof_Context.theory_of ctxt in 
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

303 
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

304 
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

305 
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

306 
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

307 
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

308 
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

309 
@{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

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

311 
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

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

313 
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

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

315 
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

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

317 
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

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

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

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

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

322 
$ 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

323 
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

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

325 
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

326 
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

327 
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

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

329 
> cterm_of thy 
39890  330 
> 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

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

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

333 
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

334 
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

335 
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

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

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

338 
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

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

340 

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

341 
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the 
42353
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

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

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

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

345 
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

346 
 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

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

348 
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

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

350 
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

351 

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

352 
(* making fact and conjecture formulas *) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

353 
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

354 
let 
42361  355 
val thy = Proof_Context.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

356 
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

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

358 
> Object_Logic.atomize_term thy 
42563  359 
val need_trueprop = (fastype_of t = @{typ bool}) 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

360 
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

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

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

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

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

365 
> kind <> Axiom ? freeze_term 
42562  366 
val (combformula, atomic_types) = 
367 
combformula_from_prop thy eq_as_iff t [] 

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

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

369 
{name = name, combformula = combformula, kind = kind, 
42562  370 
atomic_types = atomic_types} 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

372 

42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

373 
fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), t) = 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

374 
case (keep_trivial, make_formula ctxt eq_as_iff presimp name Axiom t) of 
41990
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

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

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

377 
 (_, formula) => SOME formula 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

378 

42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

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

380 
let val last = length ts  1 in 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

381 
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

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

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

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

385 

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

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

387 

42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

388 
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

389 
 formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

390 
 formula_map f (AAtom tm) = AAtom (f tm) 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

391 

024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

392 
fun formula_fold f (AQuant (_, _, phi)) = formula_fold f phi 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

393 
 formula_fold f (AConn (_, phis)) = fold (formula_fold f) phis 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

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

395 

42563  396 
type sym_table_info = 
397 
{pred_sym : bool, min_ary : int, max_ary : int, typ : typ option} 

398 

42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

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

400 
let 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

401 
fun var s = ATerm (`I s, []) 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

402 
fun tag tm = ATerm (`I type_tag_name, [var "X", tm]) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

403 
in 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

404 
Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom, 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

405 
AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

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

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

408 

42563  409 
fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_table_info) = 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

410 
case strip_prefix_and_unascii const_prefix s of 
42563  411 
SOME mangled_s => 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

412 
let 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

413 
val thy = Proof_Context.theory_of ctxt 
42563  414 
val unmangled_s = mangled_s > unmangled_const_name 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

415 
fun dub_and_inst c needs_full_types (th, j) = 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

416 
((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""), 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

417 
false), 
42566
299d4266a9f9
avoid Type.TYPE_MATCH exception for "True_or_False" for "If"
blanchet
parents:
42565
diff
changeset

418 
let val t = th > prop_of in 
299d4266a9f9
avoid Type.TYPE_MATCH exception for "True_or_False" for "If"
blanchet
parents:
42565
diff
changeset

419 
t > (general_type_arg_policy type_sys = Mangled_Types andalso 
299d4266a9f9
avoid Type.TYPE_MATCH exception for "True_or_False" for "If"
blanchet
parents:
42565
diff
changeset

420 
not (null (Term.hidden_polymorphism t))) 
299d4266a9f9
avoid Type.TYPE_MATCH exception for "True_or_False" for "If"
blanchet
parents:
42565
diff
changeset

421 
? (case typ of 
42570
77f94ac04f32
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents:
42569
diff
changeset

422 
SOME T => specialize_type thy (invert_const unmangled_s, T) 
42566
299d4266a9f9
avoid Type.TYPE_MATCH exception for "True_or_False" for "If"
blanchet
parents:
42565
diff
changeset

423 
 NONE => I) 
299d4266a9f9
avoid Type.TYPE_MATCH exception for "True_or_False" for "If"
blanchet
parents:
42565
diff
changeset

424 
end) 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

425 
fun make_facts eq_as_iff = 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

426 
map_filter (make_fact ctxt false eq_as_iff false) 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

427 
in 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

428 
metis_helpers 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

429 
> maps (fn (metis_s, (needs_full_types, ths)) => 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

430 
if metis_s <> unmangled_s orelse 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

431 
(needs_full_types andalso 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

432 
not (type_system_types_dangerous_types type_sys)) then 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

433 
[] 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

434 
else 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

435 
ths ~~ (1 upto length ths) 
42563  436 
> map (dub_and_inst mangled_s needs_full_types) 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

437 
> make_facts (not needs_full_types)) 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

438 
end 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

439 
 NONE => [] 
42563  440 
fun helper_facts_for_sym_table ctxt type_sys sym_tab = 
441 
Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab [] 

42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

442 

42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

443 
fun translate_atp_fact ctxt keep_trivial = 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

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

445 

41134  446 
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

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

449 
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

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

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

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

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

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

455 
(* Remove existing facts from the conjecture, as this can dramatically 
39005  456 
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

457 
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

458 
val goal_t = Logic.list_implies (hyp_ts, concl_t) 
42353
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

459 
val all_ts = goal_t :: fact_ts 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

460 
val subs = tfree_classes_of_terms all_ts 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

461 
val supers = tvar_classes_of_terms all_ts 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

462 
val tycons = type_consts_of_terms thy all_ts 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

463 
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

464 
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

465 
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

466 
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

467 
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

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

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

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

471 

42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

472 
fun impose_type_arg_policy type_sys = 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

473 
let 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

474 
fun aux (CombApp tmp) = CombApp (pairself aux tmp) 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

475 
 aux (CombConst (name as (s, _), ty, ty_args)) = 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

476 
(case strip_prefix_and_unascii const_prefix s of 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

477 
NONE => (name, ty_args) 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

478 
 SOME s'' => 
42570
77f94ac04f32
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents:
42569
diff
changeset

479 
let val s'' = invert_const s'' in 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

480 
case type_arg_policy type_sys s'' of 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

481 
No_Type_Args => (name, []) 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

482 
 Mangled_Types => (mangled_const_name ty_args name, []) 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

483 
 Explicit_Type_Args => (name, ty_args) 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

484 
end) 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

485 
> (fn (name, ty_args) => CombConst (name, ty, ty_args)) 
42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

486 
 aux tm = tm 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

487 
in aux end 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

488 
val impose_type_arg_policy_on_fact = 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

489 
update_combformula o formula_map o impose_type_arg_policy 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

490 

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

491 
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

492 

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

494 
(true, ATerm (class, [ATerm (name, [])])) 
42562  495 
 fo_literal_from_type_literal (TyLitFree (class, name)) = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

497 

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

499 

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

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

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

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

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

504 

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

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

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

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

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

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

510 
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

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

512 
and is_type_constr_dangerous ctxt s = 
42361  513 
let val thy = Proof_Context.theory_of ctxt in 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

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

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

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

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

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

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

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

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

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

523 

42562  524 
fun should_tag_with_type ctxt (Tags full_types) T = 
525 
full_types orelse is_type_dangerous ctxt T 

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

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

527 

42562  528 
fun type_pred_combatom type_sys T tm = 
42563  529 
CombApp (CombConst (`make_fixed_const type_pred_base, T > @{typ bool}, [T]), 
530 
tm) 

42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

531 
> impose_type_arg_policy type_sys 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

532 
> AAtom 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

533 

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

535 
let 
42556
f65e5f0341b8
fixed "tags" type encoding after latest round of changes
blanchet
parents:
42553
diff
changeset

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

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

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

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

540 
case head of 
42553
d9963b253ffa
fix handling of proxies after recent drastic changes to the type encodings
blanchet
parents:
42551
diff
changeset

541 
CombConst (name, _, ty_args) => (name, ty_args) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

543 
 CombApp _ => raise Fail "impossible \"CombApp\"" 
42562  544 
val t = ATerm (x, map fo_term_from_typ ty_args @ 
42556
f65e5f0341b8
fixed "tags" type encoding after latest round of changes
blanchet
parents:
42553
diff
changeset

545 
map (do_term false) args) 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

546 
val ty = combtyp_of u 
42530  547 
in 
42556
f65e5f0341b8
fixed "tags" type encoding after latest round of changes
blanchet
parents:
42553
diff
changeset

548 
t > (if not top_level andalso 
f65e5f0341b8
fixed "tags" type encoding after latest round of changes
blanchet
parents:
42553
diff
changeset

549 
should_tag_with_type ctxt type_sys ty then 
42562  550 
tag_with_type (fo_term_from_typ ty) 
42530  551 
else 
552 
I) 

553 
end 

42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

554 
val do_bound_type = 
42562  555 
if type_sys = Many_Typed then SOME o mangled_type_name else K NONE 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

556 
val do_out_of_bound_type = 
42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42547
diff
changeset

557 
if member (op =) [Mangled true, Args true] type_sys then 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

558 
(fn (s, ty) => 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

559 
type_pred_combatom type_sys ty (CombVar (s, ty)) 
42562  560 
> formula_from_combformula ctxt type_sys > SOME) 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

561 
else 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

562 
K NONE 
42530  563 
fun do_formula (AQuant (q, xs, phi)) = 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

564 
AQuant (q, xs > map (apsnd (fn NONE => NONE 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

565 
 SOME ty => do_bound_type ty)), 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

566 
(if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

567 
(map_filter 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

568 
(fn (_, NONE) => NONE 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

569 
 (s, SOME ty) => do_out_of_bound_type (s, ty)) xs) 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

570 
(do_formula phi)) 
42530  571 
 do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) 
42556
f65e5f0341b8
fixed "tags" type encoding after latest round of changes
blanchet
parents:
42553
diff
changeset

572 
 do_formula (AAtom tm) = AAtom (do_term true tm) 
42530  573 
in do_formula end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

574 

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

575 
fun formula_for_fact ctxt type_sys 
42562  576 
({combformula, atomic_types, ...} : translated_formula) = 
577 
mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) 

578 
(atp_type_literals_for_types type_sys Axiom atomic_types)) 

579 
(formula_from_combformula ctxt type_sys 

580 
(close_combformula_universally combformula)) 

42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

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

582 

42538
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

583 
fun logic_for_type_sys Many_Typed = Tff 
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

584 
 logic_for_type_sys _ = Fof 
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

585 

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

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

587 
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

588 
the remote provers might care. *) 
42545  589 
fun formula_line_for_fact ctxt prefix type_sys 
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

590 
(j, formula as {name, kind, ...}) = 
42538
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

591 
Formula (logic_for_type_sys type_sys, 
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

592 
prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind, 
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

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

594 

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

596 
superclass, ...}) = 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

597 
let val ty_arg = ATerm (`I "T", []) in 
42538
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

598 
Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom, 
42527
6a9458524f01
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents:
42526
diff
changeset

599 
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

600 
AAtom (ATerm (superclass, [ty_arg]))]) 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

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

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

603 

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

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

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

608 

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

610 
...}) = 
42538
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

611 
Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom, 
42562  612 
mk_ahorn (map (formula_from_fo_literal o apfst not 
613 
o fo_literal_from_arity_literal) premLits) 

614 
(formula_from_fo_literal 

615 
(fo_literal_from_arity_literal conclLit)) 

42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

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

617 

42545  618 
fun formula_line_for_conjecture ctxt type_sys 
40114  619 
({name, kind, combformula, ...} : translated_formula) = 
42538
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

620 
Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind, 
42562  621 
formula_from_combformula ctxt type_sys 
622 
(close_combformula_universally combformula) 

42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

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

624 

42562  625 
fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) = 
626 
atomic_types > atp_type_literals_for_types type_sys Conjecture 

627 
> map fo_literal_from_type_literal 

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

628 

42545  629 
fun formula_line_for_free_type j lit = 
42538
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

630 
Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis, 
42562  631 
formula_from_fo_literal lit, NONE, NONE) 
42545  632 
fun formula_lines_for_free_types type_sys facts = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

633 
let 
42353
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

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

635 
val lits = fold (union (op =)) litss [] 
42545  636 
in map2 formula_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

637 

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

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

639 

42560
7bb3796a4975
don't destroy sym table entry for special symbols such as "hAPP" if "explicit_apply" is set
blanchet
parents:
42558
diff
changeset

640 
fun add_combterm_to_sym_table explicit_apply = 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

641 
let 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

642 
fun aux top_level tm = 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

643 
let val (head, args) = strip_combterm_comb tm in 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

644 
(case head of 
42563  645 
CombConst ((s, _), T, _) => 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

646 
if String.isPrefix bound_var_prefix s then 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

647 
I 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

648 
else 
42563  649 
let val ary = length args in 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

650 
Symtab.map_default 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

651 
(s, {pred_sym = true, 
42563  652 
min_ary = if explicit_apply then 0 else ary, 
653 
max_ary = 0, typ = SOME T}) 

654 
(fn {pred_sym, min_ary, max_ary, typ} => 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

655 
{pred_sym = pred_sym andalso top_level, 
42563  656 
min_ary = Int.min (ary, min_ary), 
657 
max_ary = Int.max (ary, max_ary), 

658 
typ = if typ = SOME T then typ else NONE}) 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

659 
end 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

660 
 _ => I) 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

661 
#> fold (aux false) args 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

662 
end 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

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

664 

42560
7bb3796a4975
don't destroy sym table entry for special symbols such as "hAPP" if "explicit_apply" is set
blanchet
parents:
42558
diff
changeset

665 
val add_fact_to_sym_table = fact_lift o formula_fold o add_combterm_to_sym_table 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

666 

42557
ae0deb39a254
fixed minarity computation when "explicit_apply" is specified
blanchet
parents:
42556
diff
changeset

667 
val default_sym_table_entries = 
42563  668 
[("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}), 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

669 
(make_fixed_const predicator_base, 
42563  670 
{pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @ 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

671 
([tptp_false, tptp_true] 
42563  672 
> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE})) 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

673 

42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

674 
fun sym_table_for_facts explicit_apply facts = 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

675 
Symtab.empty > fold Symtab.default default_sym_table_entries 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

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

677 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

678 
fun min_arity_of sym_tab s = 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

679 
case Symtab.lookup sym_tab s of 
42563  680 
SOME ({min_ary, ...} : sym_table_info) => min_ary 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

681 
 NONE => 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

682 
case strip_prefix_and_unascii const_prefix s of 
42547
b5eec0c99528
fixed arity of special constants if "explicit_apply" is set
blanchet
parents:
42546
diff
changeset

683 
SOME s => 
42570
77f94ac04f32
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents:
42569
diff
changeset

684 
let val s = s > unmangled_const_name > invert_const in 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

685 
if s = predicator_base then 1 
42547
b5eec0c99528
fixed arity of special constants if "explicit_apply" is set
blanchet
parents:
42546
diff
changeset

686 
else if s = explicit_app_base then 2 
b5eec0c99528
fixed arity of special constants if "explicit_apply" is set
blanchet
parents:
42546
diff
changeset

687 
else if s = type_pred_base then 1 
42557
ae0deb39a254
fixed minarity computation when "explicit_apply" is specified
blanchet
parents:
42556
diff
changeset

688 
else 0 
42547
b5eec0c99528
fixed arity of special constants if "explicit_apply" is set
blanchet
parents:
42546
diff
changeset

689 
end 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

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

691 

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

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

693 
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

694 
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

695 
arguments and is used as a predicate. *) 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

696 
fun is_pred_sym sym_tab s = 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

697 
case Symtab.lookup sym_tab s of 
42563  698 
SOME {pred_sym, min_ary, max_ary, ...} => pred_sym andalso min_ary = max_ary 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

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

700 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

701 
val predicator_combconst = 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

702 
CombConst (`make_fixed_const predicator_base, @{typ "bool => bool"}, []) 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

703 
fun predicator tm = CombApp (predicator_combconst, tm) 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

704 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

705 
fun introduce_predicators_in_combterm sym_tab tm = 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

706 
case strip_combterm_comb tm of 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

707 
(CombConst ((s, _), _, _), _) => 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

708 
if is_pred_sym sym_tab s then tm else predicator tm 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

709 
 _ => predicator tm 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

710 

42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

711 
fun list_app head args = fold (curry (CombApp o swap)) args head 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

712 

75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

713 
fun explicit_app arg head = 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

714 
let 
42562  715 
val head_T = combtyp_of head 
716 
val (arg_T, res_T) = dest_funT head_T 

42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

717 
val explicit_app = 
42562  718 
CombConst (`make_fixed_const explicit_app_base, head_T > head_T, 
719 
[arg_T, res_T]) 

42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

720 
in list_app explicit_app [head, arg] end 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

721 
fun list_explicit_app head args = fold explicit_app args head 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

722 

42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

723 
fun introduce_explicit_apps_in_combterm sym_tab = 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

724 
let 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

725 
fun aux tm = 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

726 
case strip_combterm_comb tm of 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

727 
(head as CombConst ((s, _), _, _), args) => 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

728 
args > map aux 
42557
ae0deb39a254
fixed minarity computation when "explicit_apply" is specified
blanchet
parents:
42556
diff
changeset

729 
> chop (min_arity_of sym_tab s) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

730 
>> list_app head 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

731 
> list_explicit_app 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

732 
 (head, args) => list_explicit_app head (map aux args) 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

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

734 

42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

735 
fun firstorderize_combterm sym_tab = 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

736 
introduce_explicit_apps_in_combterm sym_tab 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

737 
#> introduce_predicators_in_combterm sym_tab 
42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

738 
val firstorderize_fact = 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

739 
update_combformula o formula_map o firstorderize_combterm 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

740 

75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

741 
fun is_const_relevant type_sys sym_tab s = 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

742 
not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

743 
(type_sys = Many_Typed orelse not (is_pred_sym sym_tab s)) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

744 

42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

745 
fun consider_combterm_consts type_sys sym_tab tm = 
42533  746 
let val (head, args) = strip_combterm_comb tm in 
747 
(case head of 

748 
CombConst ((s, s'), ty, ty_args) => 

749 
(* FIXME: exploit type subsumption *) 

42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

750 
is_const_relevant type_sys sym_tab s 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

751 
? Symtab.insert_list (op =) (s, (s', ty_args, ty)) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

752 
 _ => I) 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

753 
#> fold (consider_combterm_consts type_sys sym_tab) args 
42533  754 
end 
755 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

756 
fun consider_fact_consts type_sys sym_tab = 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

757 
fact_lift (formula_fold (consider_combterm_consts type_sys sym_tab)) 
42533  758 

42545  759 
(* FIXME: needed? *) 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

760 
fun typed_const_table_for_facts type_sys sym_tab facts = 
42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42547
diff
changeset

761 
Symtab.empty > member (op =) [Many_Typed, Mangled true, Args true] type_sys 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

762 
? fold (consider_fact_consts type_sys sym_tab) facts 
42533  763 

42562  764 
fun strip_and_map_type 0 f T = ([], f T) 
765 
 strip_and_map_type n f (Type (@{type_name fun}, [dom_T, ran_T])) = 

766 
strip_and_map_type (n  1) f ran_T >> cons (f dom_T) 

767 
 strip_and_map_type _ _ _ = raise Fail "unexpected nonfunction" 

42533  768 

42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

769 
fun problem_line_for_typed_const ctxt type_sys sym_tab s n j (s', ty_args, T) = 
42563  770 
let val ary = min_arity_of sym_tab s in 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

771 
if type_sys = Many_Typed then 
42564
d40bdf941a9a
make the problems a bit lighter by getting rid of bound quantifiers for monomorphized constants, since these always have the same return type
blanchet
parents:
42563
diff
changeset

772 
let val (arg_Ts, res_T) = strip_and_map_type ary mangled_type_name T in 
42562  773 
Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_Ts, 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

774 
(* ### FIXME: put that in typed_const_tab *) 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

775 
if is_pred_sym sym_tab s then `I tptp_tff_bool_type else res_T) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

776 
end 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

777 
else 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

778 
let 
42563  779 
val (arg_Ts, res_T) = strip_and_map_type ary I T 
42564
d40bdf941a9a
make the problems a bit lighter by getting rid of bound quantifiers for monomorphized constants, since these always have the same return type
blanchet
parents:
42563
diff
changeset

780 
val bound_names = 
d40bdf941a9a
make the problems a bit lighter by getting rid of bound quantifiers for monomorphized constants, since these always have the same return type
blanchet
parents:
42563
diff
changeset

781 
1 upto length arg_Ts > map (`I o make_bound_var o string_of_int) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

782 
val bound_tms = 
42564
d40bdf941a9a
make the problems a bit lighter by getting rid of bound quantifiers for monomorphized constants, since these always have the same return type
blanchet
parents:
42563
diff
changeset

783 
bound_names ~~ arg_Ts > map (fn (name, T) => CombConst (name, T, [])) 
42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

784 
val bound_Ts = arg_Ts > map (if n > 1 then SOME else K NONE) 
42546
8591fcc56c34
make sure typing fact names are unique (needed e.g. by SNARK)
blanchet
parents:
42545
diff
changeset

785 
val freshener = 
8591fcc56c34
make sure typing fact names are unique (needed e.g. by SNARK)
blanchet
parents:
42545
diff
changeset

786 
case type_sys of Args _ => string_of_int j ^ "_"  _ => "" 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

787 
in 
42546
8591fcc56c34
make sure typing fact names are unique (needed e.g. by SNARK)
blanchet
parents:
42545
diff
changeset

788 
Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, 
42562  789 
CombConst ((s, s'), T, ty_args) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

790 
> fold (curry (CombApp o swap)) bound_tms 
42562  791 
> type_pred_combatom type_sys res_T 
42564
d40bdf941a9a
make the problems a bit lighter by getting rid of bound quantifiers for monomorphized constants, since these always have the same return type
blanchet
parents:
42563
diff
changeset

792 
> mk_aquant AForall (bound_names ~~ bound_Ts) 
42562  793 
> formula_from_combformula ctxt type_sys, 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

794 
NONE, NONE) 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

795 
end 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

796 
end 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

797 
fun problem_lines_for_sym_decl ctxt type_sys sym_tab (s, xs) = 
42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

798 
let val n = length xs in 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

799 
map2 (problem_line_for_typed_const ctxt type_sys sym_tab s n) 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

800 
(0 upto n  1) xs 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

801 
end 
42563  802 
fun problem_lines_for_sym_decls ctxt type_sys sym_tab typed_const_tab = 
803 
Symtab.fold_rev (append o problem_lines_for_sym_decl ctxt type_sys sym_tab) 

804 
typed_const_tab [] 

42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

805 

f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

806 
fun add_tff_types_in_formula (AQuant (_, xs, phi)) = 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

807 
union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

808 
 add_tff_types_in_formula (AConn (_, phis)) = 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

809 
fold add_tff_types_in_formula phis 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

810 
 add_tff_types_in_formula (AAtom _) = I 
42539
f6ba908b8b27
generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents:
42538
diff
changeset

811 

42562  812 
fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) = 
813 
union (op =) (res_T :: arg_Ts) 

42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

814 
 add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) = 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

815 
add_tff_types_in_formula phi 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

816 

f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

817 
fun tff_types_in_problem problem = 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

818 
fold (fold add_tff_types_in_problem_line o snd) problem [] 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

819 

42545  820 
fun decl_line_for_tff_type (s, s') = 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

821 
Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_tff_type_of_types) 
42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

822 

f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

823 
val type_declsN = "Types" 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

824 
val sym_declsN = "Symbol types" 
41157  825 
val factsN = "Relevant facts" 
826 
val class_relsN = "Class relationships" 

42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

827 
val aritiesN = "Arities" 
41157  828 
val helpersN = "Helper facts" 
829 
val conjsN = "Conjectures" 

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

830 
val free_typesN = "Type variables" 
41157  831 

832 
fun offset_of_heading_in_problem _ [] j = j 

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

834 
if heading = needle then j 

835 
else offset_of_heading_in_problem needle problem (j + length lines) 

836 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

837 
fun prepare_atp_problem ctxt type_sys 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

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

839 
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = 
41134  840 
translate_formulas ctxt type_sys hyp_ts concl_t facts 
42563  841 
val sym_tab = conjs @ facts > sym_table_for_facts explicit_apply 
42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

842 
val (conjs, facts) = 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

843 
(conjs, facts) > pairself (map (firstorderize_fact sym_tab)) 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

844 
val sym_tab = conjs @ facts > sym_table_for_facts explicit_apply 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

845 
val (conjs, facts) = 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

846 
(conjs, facts) > pairself (map (impose_type_arg_policy_on_fact type_sys)) 
42563  847 
val sym_tab' = conjs @ facts > sym_table_for_facts false 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

848 
val typed_const_tab = 
42563  849 
conjs @ facts > typed_const_table_for_facts type_sys sym_tab' 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

850 
val sym_decl_lines = 
42563  851 
typed_const_tab > problem_lines_for_sym_decls ctxt type_sys sym_tab' 
852 
val helpers = helper_facts_for_sym_table ctxt type_sys sym_tab' 

42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

853 
> map (firstorderize_fact sym_tab 
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

854 
#> impose_type_arg_policy_on_fact type_sys) 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

855 
(* Reordering these might confuse the proof reconstruction code or the SPASS 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

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

857 
val problem = 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

858 
[(sym_declsN, sym_decl_lines), 
42545  859 
(factsN, map (formula_line_for_fact ctxt fact_prefix type_sys) 
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

860 
(0 upto length facts  1 ~~ facts)), 
42545  861 
(class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), 
862 
(aritiesN, map formula_line_for_arity_clause arity_clauses), 

42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

863 
(helpersN, map (formula_line_for_fact ctxt helper_prefix type_sys) 
42563  864 
(0 upto length helpers  1 ~~ helpers) 
865 
> (if type_sys = Tags false then cons (ti_ti_helper_fact ()) 

866 
else I)), 

42545  867 
(conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs), 
868 
(free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))] 

42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

869 
val problem = 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

870 
problem 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

871 
> (if type_sys = Many_Typed then 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

872 
cons (type_declsN, 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

873 
map decl_line_for_tff_type (tff_types_in_problem problem)) 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

874 
else 
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

875 
I) 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

876 
val (problem, pool) = problem > nice_atp_problem (!readable_names) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

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

879 
case pool of SOME the_pool => snd the_pool  NONE => Symtab.empty, 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42540
diff
changeset

880 
offset_of_heading_in_problem factsN problem 0, 
41157  881 
offset_of_heading_in_problem conjsN problem 0, 
882 
fact_names > Vector.fromList) 

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

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

884 

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

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

886 
val conj_weight = 0.0 
41770  887 
val hyp_weight = 0.1 
888 
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

889 
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

890 

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

891 
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

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

893 
#> fold (add_term_weights weight) tms 
42538
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

894 
fun add_problem_line_weights weight (Formula (_, _, _, phi, _, _)) = 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

895 
formula_fold (add_term_weights weight) phi 
42528  896 
 add_problem_line_weights _ _ = I 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

897 

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

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

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

900 
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

901 
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

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

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

904 

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

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

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

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

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

909 
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

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

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

912 
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

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

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

915 

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

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

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

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

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

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

921 
> Symtab.dest 
41726  922 
> 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

923 

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

924 
end; 