author  blanchet 
Sun, 01 May 2011 18:37:25 +0200  
changeset 42585  723b9d1e8ba5 
parent 42579  2552c09b1a72 
child 42586  59e0ca92bb0b 
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 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

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

15 

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

16 
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

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

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

19 
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

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

21 
val type_pred_base : string 
42562  22 
val tff_type_prefix : string 
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

23 
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

24 
val unmangled_const : string > string * string fo_term list 
41088  25 
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

26 
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

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

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

29 
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

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

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

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

33 
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

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

35 

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

36 
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

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

38 

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

39 
open ATP_Problem 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

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

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

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

43 

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

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

45 
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

46 
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

47 

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

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

49 
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

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

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

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

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

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

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

56 

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

57 
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

58 
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

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

61 

42562  62 
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

63 

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

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

65 
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

66 
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

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

68 
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

69 

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

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

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

72 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

73 
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

74 
 formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

75 
 formula_map f (AAtom tm) = AAtom (f tm) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

76 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

77 
fun formula_fold f (AQuant (_, _, phi)) = formula_fold f phi 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

78 
 formula_fold f (AConn (_, phis)) = fold (formula_fold f) phis 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

79 
 formula_fold f (AAtom tm) = f tm 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

80 

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

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

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

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

86 

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

87 
fun update_combformula f 
42562  88 
({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

89 
{name = name, kind = kind, combformula = f combformula, 
42562  90 
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

91 

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

92 
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

93 

42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

94 
fun type_sys_declares_sym_types Many_Typed = true 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

95 
 type_sys_declares_sym_types (Mangled level) = level <> Unsound 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

96 
 type_sys_declares_sym_types (Args (_, level)) = level <> Unsound 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

97 
 type_sys_declares_sym_types _ = false 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

98 

42572
0c9a947b43fc
drop "fequal" type args for unmangled type systems
blanchet
parents:
42570
diff
changeset

99 
val boring_consts = [explicit_app_base, @{const_name Metis.fequal}] 
0c9a947b43fc
drop "fequal" type args for unmangled type systems
blanchet
parents:
42570
diff
changeset

100 

0c9a947b43fc
drop "fequal" type args for unmangled type systems
blanchet
parents:
42570
diff
changeset

101 
fun should_omit_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

102 
s <> type_pred_base andalso 
42572
0c9a947b43fc
drop "fequal" type args for unmangled type systems
blanchet
parents:
42570
diff
changeset

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

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

106 
 Mangled _ => false 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

107 
 Tags (_, Sound) => true 
42572
0c9a947b43fc
drop "fequal" type args for unmangled type systems
blanchet
parents:
42570
diff
changeset

108 
 No_Types => true 
0c9a947b43fc
drop "fequal" type args for unmangled type systems
blanchet
parents:
42570
diff
changeset

109 
 _ => member (op =) boring_consts s) 
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

110 

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

111 
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

112 

42563  113 
fun general_type_arg_policy Many_Typed = Mangled_Types 
114 
 general_type_arg_policy (Mangled _) = Mangled_Types 

42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

115 
 general_type_arg_policy No_Types = No_Type_Args 
42563  116 
 general_type_arg_policy _ = Explicit_Type_Args 
117 

42524  118 
fun type_arg_policy type_sys s = 
42572
0c9a947b43fc
drop "fequal" type args for unmangled type systems
blanchet
parents:
42570
diff
changeset

119 
if should_omit_type_args type_sys s then No_Type_Args 
42563  120 
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

121 

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

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

123 
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

124 
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

125 

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

126 
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

127 
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

128 
[] 
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

129 
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

130 
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

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

132 
 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

133 

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

134 
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

135 
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

136 
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

137 
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

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

139 
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

140 
 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

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

142 
 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

143 
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

144 
 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

145 

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

146 
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

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

148 
fun formula_vars bounds (AQuant (_, xs, phi)) = 
42526  149 
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

150 
 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

151 
 formula_vars bounds (AAtom tm) = 
42526  152 
union (op =) (atom_vars tm [] 
153 
> 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

154 
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

155 

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

156 
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

157 
 combterm_vars (CombConst _) = I 
42574  158 
 combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T) 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

159 
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

160 

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

161 
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

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

164 
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

165 

42562  166 
fun fo_term_from_typ (Type (s, Ts)) = 
167 
ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts) 

168 
 fo_term_from_typ (TFree (s, _)) = 

169 
ATerm (`make_fixed_type_var s, []) 

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

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

172 

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

174 
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

175 

42562  176 
fun generic_mangled_type_name f (ATerm (name, [])) = f name 
177 
 generic_mangled_type_name f (ATerm (name, tys)) = 

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

179 
val mangled_type_name = 

180 
fo_term_from_typ 

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

182 
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

183 

42574  184 
fun generic_mangled_type_suffix f g Ts = 
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

185 
fold_rev (curry (op ^) o g o prefix mangled_type_sep 
42574  186 
o generic_mangled_type_name f) Ts "" 
42562  187 
fun mangled_const_name T_args (s, s') = 
188 
let val ty_args = map fo_term_from_typ T_args in 

189 
(s ^ generic_mangled_type_suffix fst ascii_of ty_args, 

190 
s' ^ generic_mangled_type_suffix snd I ty_args) 

191 
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

192 

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

194 
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

195 

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

196 
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

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

198 
 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

199 
[] >> 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

200 
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

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

202 

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

204 
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

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

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

207 
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

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

209 

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

210 
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

211 
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

212 
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

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

214 
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

215 

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

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

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

218 
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

219 
CombApp (aux top_level tm1, aux false tm2) 
42574  220 
 aux top_level (CombConst (name as (s, s'), T, T_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

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

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

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

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

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

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

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

228 
else 
42574  229 
(proxy_base >> prefix const_prefix, T_args) 
230 
 NONE => (name, T_args)) 

231 
> (fn (name, T_args) => CombConst (name, T, T_args)) 

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

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

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

234 

42562  235 
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

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

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

238 
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

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

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

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

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

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

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

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

247 
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

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

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

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

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

252 
 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

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

254 
 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

255 
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

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

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

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

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

260 
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

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

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

263 

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

265 

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

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

268 
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

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

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

271 
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

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

273 

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

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

276 
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

277 
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

278 
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

279 
 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

280 
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

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

282 
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

283 
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

284 
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

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

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

287 
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

288 
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

289 
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

290 
 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

291 
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

292 

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

293 
fun introduce_combinators_in_term ctxt kind t = 
42361  294 
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

295 
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

296 
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

297 
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

298 
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

299 
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

300 
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

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

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

303 
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

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

305 
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

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

307 
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

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

309 
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

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

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

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

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

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

315 
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

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

317 
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

318 
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

319 
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

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

321 
> cterm_of thy 
39890  322 
> 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

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

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

325 
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

326 
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

327 
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

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

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

330 
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

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

332 

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

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

334 
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

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

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

337 
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

338 
 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

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

340 
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

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

342 
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

343 

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

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

345 
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

346 
let 
42361  347 
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

348 
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

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

350 
> Object_Logic.atomize_term thy 
42563  351 
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

352 
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

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

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

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

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

357 
> kind <> Axiom ? freeze_term 
42562  358 
val (combformula, atomic_types) = 
359 
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

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

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

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

364 

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

365 
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

366 
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

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

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

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

370 

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

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

372 
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

373 
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

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

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

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

377 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

378 
(** "hBOOL" and "hAPP" **) 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

379 

42574  380 
type sym_info = 
42563  381 
{pred_sym : bool, min_ary : int, max_ary : int, typ : typ option} 
382 

42574  383 
fun add_combterm_syms_to_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

384 
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

385 
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

386 
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

387 
(case head of 
42563  388 
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

389 
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

390 
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

391 
else 
42563  392 
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

393 
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

394 
(s, {pred_sym = true, 
42563  395 
min_ary = if explicit_apply then 0 else ary, 
396 
max_ary = 0, typ = SOME T}) 

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

398 
{pred_sym = pred_sym andalso top_level, 
42563  399 
min_ary = Int.min (ary, min_ary), 
400 
max_ary = Int.max (ary, max_ary), 

401 
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

402 
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

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

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

405 
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

406 
in aux true end 
42574  407 
val add_fact_syms_to_table = 
408 
fact_lift o formula_fold o add_combterm_syms_to_table 

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

409 

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

410 
val default_sym_table_entries = 
42563  411 
[("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

412 
(make_fixed_const predicator_base, 
42563  413 
{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

414 
([tptp_false, tptp_true] 
42563  415 
> 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

416 

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

417 
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

418 
Symtab.empty > fold Symtab.default default_sym_table_entries 
42574  419 
> fold (add_fact_syms_to_table explicit_apply) facts 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

420 

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

421 
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

422 
case Symtab.lookup sym_tab s of 
42574  423 
SOME ({min_ary, ...} : sym_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

424 
 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

425 
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

426 
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

427 
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

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

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

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

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

432 
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

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

434 

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

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

436 
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

437 
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

438 
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

439 
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

440 
case Symtab.lookup sym_tab s of 
42574  441 
SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) => 
442 
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

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

444 

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

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

446 
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

447 
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

448 

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

449 
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

450 
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

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

452 
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

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

454 

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

455 
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

456 

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

457 
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

458 
let 
42562  459 
val head_T = combtyp_of head 
460 
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

461 
val explicit_app = 
42562  462 
CombConst (`make_fixed_const explicit_app_base, head_T > head_T, 
463 
[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

464 
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

465 
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

466 

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

467 
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

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

469 
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

470 
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

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

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

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

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

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

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

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

478 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

479 
fun impose_type_arg_policy_in_combterm type_sys = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

480 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

481 
fun aux (CombApp tmp) = CombApp (pairself aux tmp) 
42574  482 
 aux (CombConst (name as (s, _), T, T_args)) = 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

483 
(case strip_prefix_and_unascii const_prefix s of 
42574  484 
NONE => (name, T_args) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

485 
 SOME s'' => 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

486 
let val s'' = invert_const s'' in 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

487 
case type_arg_policy type_sys s'' of 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

488 
No_Type_Args => (name, []) 
42574  489 
 Mangled_Types => (mangled_const_name T_args name, []) 
490 
 Explicit_Type_Args => (name, T_args) 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

491 
end) 
42574  492 
> (fn (name, T_args) => CombConst (name, T, T_args)) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

493 
 aux tm = tm 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

494 
in aux end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

495 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

496 
fun repair_combterm type_sys sym_tab = 
42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

497 
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

498 
#> introduce_predicators_in_combterm sym_tab 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

499 
#> impose_type_arg_policy_in_combterm type_sys 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

500 
val repair_fact = update_combformula o formula_map oo repair_combterm 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

501 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

502 
(** Helper facts **) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

503 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

504 
fun ti_ti_helper_fact () = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

505 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

506 
fun var s = ATerm (`I s, []) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

507 
fun tag tm = ATerm (`I type_tag_name, [var "X", tm]) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

508 
in 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

509 
Formula (helper_prefix ^ ascii_of "ti_ti", Axiom, 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

510 
AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

511 
> close_formula_universally, NONE, NONE) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

512 
end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

513 

42574  514 
fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_info) = 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

515 
case strip_prefix_and_unascii const_prefix s of 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

516 
SOME mangled_s => 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

517 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

518 
val thy = Proof_Context.theory_of ctxt 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

519 
val unmangled_s = mangled_s > unmangled_const_name 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

520 
fun dub_and_inst c needs_some_types (th, j) = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

521 
((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""), 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

522 
false), 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

523 
let val t = th > prop_of in 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

524 
t > (general_type_arg_policy type_sys = Mangled_Types andalso 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

525 
not (null (Term.hidden_polymorphism t))) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

526 
? (case typ of 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

527 
SOME T => specialize_type thy (invert_const unmangled_s, T) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

528 
 NONE => I) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

529 
end) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

530 
fun make_facts eq_as_iff = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

531 
map_filter (make_fact ctxt false eq_as_iff false) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

532 
in 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

533 
metis_helpers 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

534 
> maps (fn (metis_s, (needs_some_types, ths)) => 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

535 
if metis_s <> unmangled_s orelse 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

536 
(needs_some_types andalso 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

537 
level_of_type_sys type_sys = Unsound) then 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

538 
[] 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

539 
else 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

540 
ths ~~ (1 upto length ths) 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

541 
> map (dub_and_inst mangled_s needs_some_types) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

542 
> make_facts (not needs_some_types)) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

543 
end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

544 
 NONE => [] 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

545 
fun helper_facts_for_sym_table ctxt type_sys sym_tab = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

546 
Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab [] 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

547 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

548 
fun translate_atp_fact ctxt keep_trivial = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

549 
`(make_fact ctxt keep_trivial true true o apsnd prop_of) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

550 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

551 
fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

552 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

553 
val thy = Proof_Context.theory_of ctxt 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

554 
val fact_ts = map (prop_of o snd o snd) rich_facts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

555 
val (facts, fact_names) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

556 
rich_facts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

557 
> map_filter (fn (NONE, _) => NONE 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

558 
 (SOME fact, (name, _)) => SOME (fact, name)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

559 
> ListPair.unzip 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

560 
(* Remove existing facts from the conjecture, as this can dramatically 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

561 
boost an ATP's performance (for some reason). *) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

562 
val hyp_ts = hyp_ts > filter_out (member (op aconv) fact_ts) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

563 
val goal_t = Logic.list_implies (hyp_ts, concl_t) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

564 
val all_ts = goal_t :: fact_ts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

565 
val subs = tfree_classes_of_terms all_ts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

566 
val supers = tvar_classes_of_terms all_ts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

567 
val tycons = type_consts_of_terms thy all_ts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

568 
val conjs = make_conjecture ctxt (hyp_ts @ [concl_t]) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

569 
val (supers', arity_clauses) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

570 
if type_sys = No_Types then ([], []) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

571 
else make_arity_clauses thy tycons supers 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

572 
val class_rel_clauses = make_class_rel_clauses thy subs supers' 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

573 
in 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

574 
(fact_names > map single, (conjs, facts, class_rel_clauses, arity_clauses)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

575 
end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

576 

42574  577 
fun tag_with_type ty tm = ATerm (`I type_tag_name, [ty, tm]) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

578 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

579 
fun fo_literal_from_type_literal (TyLitVar (class, name)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

580 
(true, ATerm (class, [ATerm (name, [])])) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

581 
 fo_literal_from_type_literal (TyLitFree (class, name)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

582 
(true, ATerm (class, [ATerm (name, [])])) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

583 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

584 
fun formula_from_fo_literal (pos, t) = AAtom t > not pos ? mk_anot 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

585 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

586 
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

587 
considered dangerous because their "exhaust" properties can easily lead to 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

588 
unsound ATP proofs. The checks below are an (unsound) approximation of 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

589 
finiteness. *) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

590 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

591 
fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

592 
 is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

593 
is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

594 
 is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

595 
and is_type_dangerous ctxt (Type (s, Ts)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

596 
is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

597 
 is_type_dangerous _ _ = false 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

598 
and is_type_constr_dangerous ctxt s = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

599 
let val thy = Proof_Context.theory_of ctxt in 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

600 
case Datatype_Data.get_info thy s of 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

601 
SOME {descr, ...} => 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

602 
forall (fn (_, (_, _, constrs)) => 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

603 
forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

604 
 NONE => 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

605 
case Typedef.get_info ctxt s of 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

606 
({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

607 
 [] => true 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

608 
end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

609 

42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

610 
fun should_encode_type _ Sound _ = true 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

611 
 should_encode_type ctxt Half_Sound T = is_type_dangerous ctxt T 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

612 
 should_encode_type _ Unsound _ = false 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

613 

2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

614 
fun should_tag_with_type ctxt (Tags (_, level)) T = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

615 
should_encode_type ctxt level T 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

616 
 should_tag_with_type _ _ _ = false 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

617 

42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

618 
fun should_predicate_on_type ctxt (Mangled level) T = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

619 
should_encode_type ctxt level T 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

620 
 should_predicate_on_type ctxt (Args (_, level)) T = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

621 
should_encode_type ctxt level T 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

622 
 should_predicate_on_type _ _ _ = false 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

623 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

624 
fun type_pred_combatom type_sys T tm = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

625 
CombApp (CombConst (`make_fixed_const type_pred_base, T > @{typ bool}, [T]), 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

626 
tm) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

627 
> impose_type_arg_policy_in_combterm type_sys 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

628 
> AAtom 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

629 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

630 
fun formula_from_combformula ctxt type_sys = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

631 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

632 
fun do_term top_level u = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

633 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

634 
val (head, args) = strip_combterm_comb u 
42574  635 
val (x, T_args) = 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

636 
case head of 
42574  637 
CombConst (name, _, T_args) => (name, T_args) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

638 
 CombVar (name, _) => (name, []) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

639 
 CombApp _ => raise Fail "impossible \"CombApp\"" 
42574  640 
val t = ATerm (x, map fo_term_from_typ T_args @ 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

641 
map (do_term false) args) 
42574  642 
val T = combtyp_of u 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

643 
in 
42574  644 
t > (if not top_level andalso should_tag_with_type ctxt type_sys T then 
645 
tag_with_type (fo_term_from_typ T) 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

646 
else 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

647 
I) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

648 
end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

649 
val do_bound_type = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

650 
if type_sys = Many_Typed then SOME o mangled_type_name else K NONE 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

651 
fun do_out_of_bound_type (s, T) = 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

652 
if should_predicate_on_type ctxt type_sys T then 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

653 
type_pred_combatom type_sys T (CombVar (s, T)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

654 
> do_formula > SOME 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

655 
else 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

656 
NONE 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

657 
and do_formula (AQuant (q, xs, phi)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

658 
AQuant (q, xs > map (apsnd (fn NONE => NONE 
42574  659 
 SOME T => do_bound_type T)), 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

660 
(if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

661 
(map_filter 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

662 
(fn (_, NONE) => NONE 
42574  663 
 (s, SOME T) => do_out_of_bound_type (s, T)) xs) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

664 
(do_formula phi)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

665 
 do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

666 
 do_formula (AAtom tm) = AAtom (do_term true tm) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

667 
in do_formula end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

668 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

669 
fun formula_for_fact ctxt type_sys 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

670 
({combformula, atomic_types, ...} : translated_formula) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

671 
mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

672 
(atp_type_literals_for_types type_sys Axiom atomic_types)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

673 
(formula_from_combformula ctxt type_sys 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

674 
(close_combformula_universally combformula)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

675 
> close_formula_universally 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

676 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

677 
(* Each fact is given a unique fact number to avoid name clashes (e.g., because 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

678 
of monomorphization). The TPTP explicitly forbids name clashes, and some of 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

679 
the remote provers might care. *) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

680 
fun formula_line_for_fact ctxt prefix type_sys 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

681 
(j, formula as {name, kind, ...}) = 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

682 
Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind, 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

683 
formula_for_fact ctxt type_sys formula, NONE, NONE) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

684 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

685 
fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass, 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

686 
superclass, ...}) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

687 
let val ty_arg = ATerm (`I "T", []) in 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

688 
Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

689 
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

690 
AAtom (ATerm (superclass, [ty_arg]))]) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

691 
> close_formula_universally, NONE, NONE) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

692 
end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

693 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

694 
fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

695 
(true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

696 
 fo_literal_from_arity_literal (TVarLit (c, sort)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

697 
(false, ATerm (c, [ATerm (sort, [])])) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

698 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

699 
fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits, 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

700 
...}) = 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

701 
Formula (arity_clause_prefix ^ ascii_of name, Axiom, 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

702 
mk_ahorn (map (formula_from_fo_literal o apfst not 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

703 
o fo_literal_from_arity_literal) premLits) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

704 
(formula_from_fo_literal 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

705 
(fo_literal_from_arity_literal conclLit)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

706 
> close_formula_universally, NONE, NONE) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

707 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

708 
fun formula_line_for_conjecture ctxt type_sys 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

709 
({name, kind, combformula, ...} : translated_formula) = 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

710 
Formula (conjecture_prefix ^ name, kind, 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

711 
formula_from_combformula ctxt type_sys 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

712 
(close_combformula_universally combformula) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

713 
> close_formula_universally, NONE, NONE) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

714 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

715 
fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

716 
atomic_types > atp_type_literals_for_types type_sys Conjecture 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

717 
> map fo_literal_from_type_literal 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

718 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

719 
fun formula_line_for_free_type j lit = 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

720 
Formula (tfree_prefix ^ string_of_int j, Hypothesis, 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

721 
formula_from_fo_literal lit, NONE, NONE) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

722 
fun formula_lines_for_free_types type_sys facts = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

723 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

724 
val litss = map (free_type_literals type_sys) facts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

725 
val lits = fold (union (op =)) litss [] 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

726 
in map2 formula_line_for_free_type (0 upto length lits  1) lits end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

727 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

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

729 

42574  730 
fun should_declare_sym type_sys pred_sym 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

731 
not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso 
42574  732 
(type_sys = Many_Typed orelse not pred_sym) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

733 

42574  734 
fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab = 
735 
let 

42576
a8a80a2a34be
merge symbol declarations that are typeinstances of each other  useful for type system "Args true" with monomorphization turned off
blanchet
parents:
42575
diff
changeset

736 
fun declare_sym (decl as (_, _, T, _, _)) decls = 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

737 
case type_sys of 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

738 
Tags (false, Sound) => 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

739 
if exists (curry Type.raw_instance T o #3) decls then 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

740 
decls 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

741 
else 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

742 
decl :: filter_out ((fn T' => Type.raw_instance (T', T)) o #3) decls 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

743 
 _ => insert (op =) decl decls 
42576
a8a80a2a34be
merge symbol declarations that are typeinstances of each other  useful for type system "Args true" with monomorphization turned off
blanchet
parents:
42575
diff
changeset

744 
fun do_term tm = 
42574  745 
let val (head, args) = strip_combterm_comb tm in 
746 
(case head of 

747 
CombConst ((s, s'), T, T_args) => 

748 
let val pred_sym = is_pred_sym repaired_sym_tab s in 

749 
if should_declare_sym type_sys pred_sym s then 

42576
a8a80a2a34be
merge symbol declarations that are typeinstances of each other  useful for type system "Args true" with monomorphization turned off
blanchet
parents:
42575
diff
changeset

750 
Symtab.map_default (s, []) 
a8a80a2a34be
merge symbol declarations that are typeinstances of each other  useful for type system "Args true" with monomorphization turned off
blanchet
parents:
42575
diff
changeset

751 
(declare_sym (s', T_args, T, pred_sym, length args)) 
42574  752 
else 
753 
I 

754 
end 

755 
 _ => I) 

42576
a8a80a2a34be
merge symbol declarations that are typeinstances of each other  useful for type system "Args true" with monomorphization turned off
blanchet
parents:
42575
diff
changeset

756 
#> fold do_term args 
42574  757 
end 
42576
a8a80a2a34be
merge symbol declarations that are typeinstances of each other  useful for type system "Args true" with monomorphization turned off
blanchet
parents:
42575
diff
changeset

758 
in do_term end 
42574  759 
fun add_fact_syms_to_decl_table type_sys repaired_sym_tab = 
760 
fact_lift (formula_fold 

761 
(add_combterm_syms_to_decl_table type_sys repaired_sym_tab)) 

762 
fun sym_decl_table_for_facts type_sys repaired_sym_tab facts = 

42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

763 
Symtab.empty > type_sys_declares_sym_types type_sys 
42574  764 
? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab) 
765 
facts 

42533  766 

42574  767 
fun n_ary_strip_type 0 T = ([], T) 
768 
 n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) = 

769 
n_ary_strip_type (n  1) ran_T >> cons dom_T 

770 
 n_ary_strip_type _ _ = raise Fail "unexpected nonfunction" 

42533  771 

42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

772 
fun result_type_of_decl (_, _, T, _, ary) = n_ary_strip_type ary T > snd 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

773 

2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

774 
fun decl_line_for_sym_decl s (s', _, T, pred_sym, ary) = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

775 
let val (arg_Ts, res_T) = n_ary_strip_type ary T in 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

776 
Decl (sym_decl_prefix ^ ascii_of s, (s, s'), 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

777 
map mangled_type_name arg_Ts, 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

778 
if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

779 
end 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

780 

2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

781 
fun formula_line_for_sym_decl ctxt type_sys n s j (s', T_args, T, _, ary) = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

782 
let 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

783 
val (arg_Ts, res_T) = n_ary_strip_type ary T 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

784 
val bound_names = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

785 
1 upto length arg_Ts > map (`I o make_bound_var o string_of_int) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

786 
val bound_tms = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

787 
bound_names ~~ arg_Ts > map (fn (name, T) => CombConst (name, T, [])) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

788 
val bound_Ts = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

789 
arg_Ts > map (if n > 1 then SOME else K NONE) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

790 
val freshener = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

791 
case type_sys of Args _ => string_of_int j ^ "_"  _ => "" 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

792 
in 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

793 
Formula (sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

794 
CombConst ((s, s'), T, T_args) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

795 
> fold (curry (CombApp o swap)) bound_tms 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

796 
> type_pred_combatom type_sys res_T 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

797 
> mk_aquant AForall (bound_names ~~ bound_Ts) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

798 
> formula_from_combformula ctxt type_sys, 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

799 
NONE, NONE) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

800 
end 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

801 

2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

802 
fun problem_lines_for_sym_decls ctxt type_sys (s, decls) = 
42574  803 
if type_sys = Many_Typed then 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

804 
map (decl_line_for_sym_decl s) decls 
42574  805 
else 
806 
let 

42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

807 
val decls = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

808 
case decls of 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

809 
decl :: (decls' as _ :: _) => 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

810 
if forall (curry (op =) (result_type_of_decl decl) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

811 
o result_type_of_decl) decls' then 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

812 
[decl] 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

813 
else 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

814 
decls 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

815 
 _ => decls 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

816 
val n = length decls 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

817 
val decls = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

818 
decls > filter (should_predicate_on_type ctxt type_sys 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

819 
o result_type_of_decl) 
42574  820 
in 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

821 
map2 (formula_line_for_sym_decl ctxt type_sys n s) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

822 
(0 upto length decls  1) decls 
42574  823 
end 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

824 

42574  825 
fun problem_lines_for_sym_decl_table ctxt type_sys sym_decl_tab = 
826 
Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt type_sys) 

827 
sym_decl_tab [] 

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

828 

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

829 
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

830 
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

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

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

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

834 

42562  835 
fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) = 
836 
union (op =) (res_T :: arg_Ts) 

42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

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

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

839 

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

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

841 
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

842 

42545  843 
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

844 
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

845 

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

846 
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

847 
val sym_declsN = "Symbol types" 
41157  848 
val factsN = "Relevant facts" 
849 
val class_relsN = "Class relationships" 

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

850 
val aritiesN = "Arities" 
41157  851 
val helpersN = "Helper facts" 
852 
val conjsN = "Conjectures" 

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

853 
val free_typesN = "Type variables" 
41157  854 

855 
fun offset_of_heading_in_problem _ [] j = j 

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

857 
if heading = needle then j 

858 
else offset_of_heading_in_problem needle problem (j + length lines) 

859 

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

860 
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

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

862 
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = 
41134  863 
translate_formulas ctxt type_sys hyp_ts concl_t facts 
42563  864 
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

865 
val (conjs, facts) = 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

866 
(conjs, facts) > pairself (map (repair_fact type_sys sym_tab)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

867 
val repaired_sym_tab = conjs @ facts > sym_table_for_facts false 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

868 
val sym_decl_lines = 
42574  869 
conjs @ facts 
870 
> sym_decl_table_for_facts type_sys repaired_sym_tab 

871 
> problem_lines_for_sym_decl_table ctxt type_sys 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

872 
val helpers = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

873 
helper_facts_for_sym_table ctxt type_sys repaired_sym_tab 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

874 
> map (repair_fact type_sys sym_tab) 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

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

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

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

878 
[(sym_declsN, sym_decl_lines), 
42545  879 
(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

880 
(0 upto length facts  1 ~~ facts)), 
42545  881 
(class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), 
882 
(aritiesN, map formula_line_for_arity_clause arity_clauses), 

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

883 
(helpersN, map (formula_line_for_fact ctxt helper_prefix type_sys) 
42563  884 
(0 upto length helpers  1 ~~ helpers) 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

885 
> (case type_sys of 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

886 
Tags (_, Half_Sound) => cons (ti_ti_helper_fact ()) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

887 
 _ => I)), 
42545  888 
(conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs), 
889 
(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

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

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

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

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

894 
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

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

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

897 
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

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

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

900 
case pool of SOME the_pool => snd the_pool  NONE => Symtab.empty, 
42585
723b9d1e8ba5
fixed embarrassing bug where conjecture and fact offsets were swapped
blanchet
parents:
42579
diff
changeset

901 
offset_of_heading_in_problem conjsN problem 0, 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42540
diff
changeset

902 
offset_of_heading_in_problem factsN problem 0, 
41157  903 
fact_names > Vector.fromList) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

905 

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

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

907 
val conj_weight = 0.0 
41770  908 
val hyp_weight = 0.1 
909 
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

910 
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

911 

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

912 
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

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

914 
#> fold (add_term_weights weight) tms 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

915 
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

916 
formula_fold (add_term_weights weight) phi 
42528  917 
 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

918 

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

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

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

921 
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

922 
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

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

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

925 

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

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

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

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

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

930 
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

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

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

933 
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

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

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

936 

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

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

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

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

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

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

942 
> Symtab.dest 
41726  943 
> 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

944 

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

945 
end; 