author  blanchet 
Sun, 01 May 2011 18:37:24 +0200  
changeset 42538  9e3e45636459 
parent 42534  46e690db16b8 
child 42539  f6ba908b8b27 
permissions  rwrr 
40114  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

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

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

5 

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

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

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

8 

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

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

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

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

14 

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

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

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

19 
Mangled of bool  
41134  20 
No_Types 
21 

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

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

23 
val conjecture_prefix : string 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

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

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

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

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

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

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

31 
val prepare_atp_problem : 
42521
02df3b78a438
get rid of "explicit_forall" proverspecific option, even if that means some clutter  foralls will be necessary to attach types to variables
blanchet
parents:
42520
diff
changeset

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

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

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

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

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

37 

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

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

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

40 

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

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

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

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

44 

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

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

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

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

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

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

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

52 

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

53 
val is_base = "is" 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

54 
val type_prefix = "ty_" 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

55 

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

56 
fun make_type ty = type_prefix ^ ascii_of ty 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

57 

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

58 
(* official TPTP TFF syntax *) 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

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

60 

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

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

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

63 

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

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

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

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

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

69 

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

71 
Many_Typed  
41134  72 
Tags of bool  
42523
08346ea46a59
added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents:
42522
diff
changeset

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

74 
Mangled of bool  
41134  75 
No_Types 
76 

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

77 
fun is_type_system_sound Many_Typed = true 
08346ea46a59
added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents:
42522
diff
changeset

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

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

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

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

82 

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

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

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

85 

42524  86 
fun dont_need_type_args type_sys s = 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

87 
s <> is_base andalso 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

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

89 
case type_sys of 
42533  90 
Many_Typed => false 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

91 
 Tags full_types => full_types 
42533  92 
 Args _ => false 
93 
 Mangled _ => false 

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

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

95 

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

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

97 

42524  98 
fun type_arg_policy type_sys s = 
42533  99 
if dont_need_type_args type_sys s then 
100 
No_Type_Args 

101 
else 

102 
case type_sys of 

103 
Many_Typed => Mangled_Types 

104 
 Mangled _ => Mangled_Types 

105 
 _ => Explicit_Type_Args 

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

106 

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

107 
fun num_atp_type_args thy type_sys s = 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

108 
if type_arg_policy type_sys s = Explicit_Type_Args then 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

109 
if s = is_base then 1 else num_type_args thy s 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

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

111 
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

112 

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

113 
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

114 
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

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

116 
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

117 
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

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

119 
 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

120 

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

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

122 
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

123 
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

124 
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

125 
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

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

127 
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

128 
 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

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

130 
 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

131 
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

132 
 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

133 

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

134 
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

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

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

138 
 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

139 
 formula_vars bounds (AAtom tm) = 
42526  140 
union (op =) (atom_vars tm [] 
141 
> 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

142 
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

143 

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

144 
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

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

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

147 
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

148 

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

149 
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

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

152 
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

153 

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

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

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

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

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

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

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

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

161 
do_formula ((s, T) :: bs) t' 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

162 
#>> mk_aquant q [(`make_bound_var s, SOME (combtyp_from_typ T))] 
38518
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

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

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

165 
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

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

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

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

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

170 
 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

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

172 
 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

173 
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

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

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

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

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

178 
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

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

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

181 

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

183 

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

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

186 
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

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

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

189 
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

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

191 

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

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

194 
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

195 
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

196 
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

197 
 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

198 
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

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

200 
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

201 
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

202 
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

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

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

205 
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

206 
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

207 
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

208 
 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

209 
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

210 

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

211 
fun introduce_combinators_in_term ctxt kind t = 
42361  212 
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

213 
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

214 
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

215 
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

216 
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

217 
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

218 
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

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

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

221 
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

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

223 
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

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

225 
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

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

227 
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

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

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

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

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

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

233 
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

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

235 
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

236 
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

237 
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

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

239 
> cterm_of thy 
39890  240 
> 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

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

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

243 
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

244 
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

245 
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

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

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

248 
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

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

250 

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

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

252 
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

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

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

255 
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

256 
 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

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

258 
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

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

260 
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

261 

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

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

263 
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

264 
let 
42361  265 
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

266 
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

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

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

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

270 
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

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

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

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

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

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

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

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

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

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

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

281 

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

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

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

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

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

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

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

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

289 
let val last = length ts  1 in 
41491  290 
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

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

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

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

294 

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

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

296 

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

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

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

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

300 

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

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

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

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

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

306 

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

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

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

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

310 

42521
02df3b78a438
get rid of "explicit_forall" proverspecific option, even if that means some clutter  foralls will be necessary to attach types to variables
blanchet
parents:
42520
diff
changeset

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

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

313 
val no_dangerous_types = type_system_types_dangerous_types type_sys 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

336 
AAtom (ATerm (`I "equal", 
6a9458524f01
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents:
42526
diff
changeset

337 
[tag (tag (var "Y")), tag (var "Y")])) 
42529
747736d8b47e
added "useful_info" argument to ATP formulas  this will probably be useful later to specify intro, simp, elim to SPASS
blanchet
parents:
42528
diff
changeset

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

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

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

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

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

343 

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

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

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

346 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

363 
val tycons = type_consts_of_terms thy all_ts 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

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

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

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

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

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

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

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

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

372 

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

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

374 

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

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

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

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

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

379 

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

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

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

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

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

384 

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

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

386 

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

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

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

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

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

391 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

410 

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

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

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

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

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

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

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

417 

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

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

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

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

421 

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

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

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

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

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

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

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

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

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

430 

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

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

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

433 

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

434 
fun mangled_combtyp_component f (CombTFree name) = f name 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

435 
 mangled_combtyp_component f (CombTVar name) = 
42236
2088895a37c6
temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception
blanchet
parents:
42233
diff
changeset

436 
f name (* FIXME: shouldn't happen *) 
2088895a37c6
temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception
blanchet
parents:
42233
diff
changeset

437 
(* raise Fail "impossible schematic type variable" *) 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

438 
 mangled_combtyp_component f (CombType (name, tys)) = 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

439 
"(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")" ^ f name 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

440 

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

441 
fun mangled_combtyp ty = 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

442 
(make_type (mangled_combtyp_component fst ty), 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

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

444 

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

445 
fun mangled_type_suffix f g tys = 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

446 
fold_rev (curry (op ^) o g o prefix mangled_type_sep 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

447 
o mangled_combtyp_component f) tys "" 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

448 

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

449 
fun mangled_const_fst ty_args s = s ^ mangled_type_suffix fst ascii_of ty_args 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

450 
fun mangled_const_snd ty_args s' = s' ^ mangled_type_suffix snd I ty_args 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

451 
fun mangled_const ty_args (s, s') = 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

452 
(mangled_const_fst ty_args s, mangled_const_snd ty_args s') 
42533  453 

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

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

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

456 

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

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

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

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

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

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

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

463 

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

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

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

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

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

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

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

470 

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

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

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

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

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

475 

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

476 
fun pred_combtyp ty = 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

477 
case combtyp_from_typ @{typ "unit => bool"} of 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

478 
CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty]) 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

479 
 _ => raise Fail "expected twoargument type constructor" 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

480 

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

481 
fun has_type_combatom ty tm = 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

482 
CombApp (CombConst ((const_prefix ^ is_base, is_base), pred_combtyp ty, [ty]), 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

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

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

485 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

507 
let val s'' = invert_const s'' in 
42524  508 
case type_arg_policy type_sys s'' of 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

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

510 
 Explicit_Type_Args => (name, ty_args) 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

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

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

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

514 
 CombApp _ => raise Fail "impossible \"CombApp\"" 
42530  515 
val t = ATerm (x, map fo_term_for_combtyp ty_args @ 
516 
map (do_term false) args) 

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

517 
val ty = combtyp_of u 
42530  518 
in 
519 
t > (if should_tag_with_type ctxt type_sys ty then 

520 
tag_with_type (fo_term_for_combtyp ty) 

521 
else 

522 
I) 

523 
end 

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

524 
val do_bound_type = 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

525 
if type_sys = Many_Typed then SOME o mangled_combtyp else K NONE 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

526 
val do_out_of_bound_type = 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

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

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

529 
has_type_combatom ty (CombVar (s, ty)) 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

530 
> formula_for_combformula ctxt type_sys > SOME) 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

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

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

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

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

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

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

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

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

540 
(do_formula phi)) 
42530  541 
 do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) 
542 
 do_formula (AAtom tm) = AAtom (do_term true tm) 

543 
in do_formula end 

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

544 

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

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

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

547 
mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) 
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

548 
(atp_type_literals_for_types type_sys Axiom ctypes_sorts)) 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

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

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

551 

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

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

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

554 

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

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

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

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

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

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

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

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

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

563 

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

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

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

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

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

568 
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), 
42529
747736d8b47e
added "useful_info" argument to ATP formulas  this will probably be useful later to specify intro, simp, elim to SPASS
blanchet
parents:
42528
diff
changeset

569 
AAtom (ATerm (superclass, [ty_arg]))]), 
747736d8b47e
added "useful_info" argument to ATP formulas  this will probably be useful later to specify intro, simp, elim to SPASS
blanchet
parents:
42528
diff
changeset

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

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

572 

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

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

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

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

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

577 

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

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

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

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

581 
mk_ahorn (map (formula_for_fo_literal o apfst not 
6a9458524f01
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents:
42526
diff
changeset

582 
o fo_literal_for_arity_literal) premLits) 
6a9458524f01
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents:
42526
diff
changeset

583 
(formula_for_fo_literal 
42529
747736d8b47e
added "useful_info" argument to ATP formulas  this will probably be useful later to specify intro, simp, elim to SPASS
blanchet
parents:
42528
diff
changeset

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

585 

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

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

588 
Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind, 
42527
6a9458524f01
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents:
42526
diff
changeset

589 
formula_for_combformula ctxt type_sys 
6a9458524f01
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents:
42526
diff
changeset

590 
(close_combformula_universally combformula), 
42529
747736d8b47e
added "useful_info" argument to ATP formulas  this will probably be useful later to specify intro, simp, elim to SPASS
blanchet
parents:
42528
diff
changeset

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

592 

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

593 
fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) = 
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

594 
ctypes_sorts > atp_type_literals_for_types type_sys 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

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

596 

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

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

598 
Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis, 
42529
747736d8b47e
added "useful_info" argument to ATP formulas  this will probably be useful later to specify intro, simp, elim to SPASS
blanchet
parents:
42528
diff
changeset

599 
formula_for_fo_literal lit, NONE, NONE) 
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

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

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

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

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

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

605 

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

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

607 

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

609 

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

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

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

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

615 
Symtab.map_default 
42520  616 
(s, {min_arity = n, max_arity = 0, fun_sym = false}) 
617 
(fn {min_arity, max_arity, fun_sym} => 

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

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

619 
max_arity = Int.max (n, max_arity), 
42520  620 
fun_sym = fun_sym orelse not top_level}) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

621 
end) 
42533  622 
#> fold (consider_term_syms (top_level andalso s = type_tag_name)) ts 
623 
val consider_formula_syms = fold_formula (consider_term_syms true) 

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

624 

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

626 
 consider_problem_line_syms (Formula (_, _, _, phi, _, _)) = 
42533  627 
consider_formula_syms phi 
628 
fun consider_problem_syms problem = 

629 
fold (fold consider_problem_line_syms o snd) problem 

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

630 

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

631 
(* needed for helper facts if the problem otherwise does not involve equality *) 
42520  632 
val equal_entry = ("equal", {min_arity = 2, max_arity = 2, fun_sym = false}) 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

633 

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

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

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

637 
else 
42527
6a9458524f01
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents:
42526
diff
changeset

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

640 

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

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

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

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

645 
16383 (* large number *) 
38748  646 
else case strip_prefix_and_unascii const_prefix s of 
42524  647 
SOME s' => s' > unmangled_const > fst > invert_const 
648 
> num_atp_type_args thy type_sys 

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

649 
 NONE => 0) 
42520  650 
 min_arity_of _ _ (SOME sym_tab) s = 
651 
case Symtab.lookup sym_tab s of 

652 
SOME ({min_arity, ...} : sym_info) => min_arity 

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

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

654 

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

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

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

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

658 

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

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

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

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

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

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

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

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

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

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

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

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

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

671 

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

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

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

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

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

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

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

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

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

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

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

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

685 

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

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

687 

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

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

689 
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

690 
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

691 
arguments and is used as a predicate. *) 
42520  692 
fun is_pred_sym NONE s = 
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38518
diff
changeset

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

694 
String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s 
42520  695 
 is_pred_sym (SOME sym_tab) s = 
696 
case Symtab.lookup sym_tab s of 

697 
SOME {min_arity, max_arity, fun_sym} => 

698 
not fun_sym andalso min_arity = max_arity 

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

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

700 

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

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

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

704 
[_, t' as ATerm ((s', _), _)] => 
42520  705 
if is_pred_sym pred_sym_tab s' then t' else boolify t 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

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

707 
else 
42520  708 
t > not (is_pred_sym pred_sym_tab s) ? boolify 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

709 

42521
02df3b78a438
get rid of "explicit_forall" proverspecific option, even if that means some clutter  foralls will be necessary to attach types to variables
blanchet
parents:
42520
diff
changeset

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

711 
let 
42520  712 
val pred_sym_tab = case type_sys of Tags _ => NONE  _ => sym_tab 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

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

715 
 aux (AAtom tm) = 
42520  716 
AAtom (tm > repair_applications_in_term thy type_sys sym_tab 
717 
> repair_predicates_in_term pred_sym_tab) 

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

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

719 

42527
6a9458524f01
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents:
42526
diff
changeset

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

721 
(Formula (logic, ident, kind, phi, source, useful_info)) = 
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

722 
Formula (logic, ident, kind, repair_formula thy type_sys sym_tab phi, 
9e3e45636459
generate pure TFF problems  ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents:
42534
diff
changeset

723 
source, useful_info) 
42528  724 
 repair_problem_line _ _ _ _ = raise Fail "unexpected nonformula" 
42521
02df3b78a438
get rid of "explicit_forall" proverspecific option, even if that means some clutter  foralls will be necessary to attach types to variables
blanchet
parents:
42520
diff
changeset

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

726 

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

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

728 
not (String.isPrefix bound_var_prefix unmangled_s) andalso 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

729 
unmangled_s <> "equal" andalso 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

730 
(type_sys = Many_Typed orelse not (is_pred_sym sym_tab s)) 
42533  731 

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

732 
fun consider_combterm_consts type_sys sym_tab tm = 
42533  733 
let val (head, args) = strip_combterm_comb tm in 
734 
(case head of 

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

736 
(* FIXME: exploit type subsumption *) 

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

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

738 
(s > member (op =) [Many_Typed, Mangled true] type_sys 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

739 
? mangled_const_fst ty_args) 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

740 
? Symtab.insert_list (op =) (s, (s', ty_args, ty)) 
42533  741 
 _ => I) (* FIXME: hAPP on var *) 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

742 
#> fold (consider_combterm_consts type_sys sym_tab) args 
42533  743 
end 
744 

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

745 
fun consider_fact_consts type_sys sym_tab 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

746 
({combformula, ...} : translated_formula) = 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

747 
fold_formula (consider_combterm_consts type_sys sym_tab) combformula 
42533  748 

749 
fun const_table_for_facts type_sys sym_tab facts = 

750 
Symtab.empty > member (op =) [Many_Typed, Args true, Mangled true] type_sys 

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

751 
? fold (consider_fact_consts type_sys sym_tab) facts 
42533  752 

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

753 
fun strip_and_map_combtyp f (ty as CombType ((s, _), tys)) = 
42533  754 
(case (strip_prefix_and_unascii type_const_prefix s, tys) of 
755 
(SOME @{type_name fun}, [dom_ty, ran_ty]) => 

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

756 
strip_and_map_combtyp f ran_ty >> cons (f dom_ty) 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

757 
 _ => ([], f ty)) 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

758 
 strip_and_map_combtyp f ty = ([], f ty) 
42533  759 

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

760 
fun type_decl_line_for_const_entry ctxt type_sys sym_tab s (s', ty_args, ty) = 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

761 
if type_sys = Many_Typed then 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

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

763 
val (arg_tys, res_ty) = strip_and_map_combtyp mangled_combtyp ty 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

764 
val (s, s') = (s, s') > mangled_const ty_args 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

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

766 
Type_Decl (type_decl_prefix ^ ascii_of s, (s, s'), arg_tys, 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

767 
if is_pred_sym sym_tab s then `I tff_bool_type else res_ty) 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

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

769 
else 
42533  770 
let 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

771 
val (arg_tys, res_ty) = strip_and_map_combtyp I ty 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

772 
val bounds = 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

773 
map (`I o make_bound_var o string_of_int) (1 upto length arg_tys) 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

774 
~~ map SOME arg_tys 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

775 
val bound_tms = 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

776 
map (fn (name, ty) => CombConst (name, the ty, [])) bounds 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

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

778 
Formula (Fof, type_decl_prefix ^ ascii_of s, Axiom, 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

779 
mk_aquant AForall bounds 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

780 
(has_type_combatom res_ty 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

781 
(fold (curry (CombApp o swap)) bound_tms 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

782 
(CombConst ((s, s'), ty, ty_args)))) 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

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

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

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

786 
fun type_decl_lines_for_const ctxt type_sys sym_tab (s, xs) = 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

787 
map (type_decl_line_for_const_entry ctxt type_sys sym_tab s) xs 
42533  788 

41157  789 
val factsN = "Relevant facts" 
790 
val class_relsN = "Class relationships" 

791 
val aritiesN = "Arity declarations" 

792 
val helpersN = "Helper facts" 

42533  793 
val type_declsN = "Type declarations" 
41157  794 
val conjsN = "Conjectures" 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

795 
val free_typesN = "Type variables" 
41157  796 

797 
fun offset_of_heading_in_problem _ [] j = j 

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

799 
if heading = needle then j 

800 
else offset_of_heading_in_problem needle problem (j + length lines) 

801 

42521
02df3b78a438
get rid of "explicit_forall" proverspecific option, even if that means some clutter  foralls will be necessary to attach types to variables
blanchet
parents:
42520
diff
changeset

802 
fun prepare_atp_problem ctxt readable_names type_sys explicit_apply hyp_ts 
02df3b78a438
get rid of "explicit_forall" proverspecific option, even if that means some clutter  foralls will be necessary to attach types to variables
blanchet
parents:
42520
diff
changeset

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

804 
let 
42361  805 
val thy = Proof_Context.theory_of ctxt 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

806 
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = 
41134  807 
translate_formulas ctxt type_sys hyp_ts concl_t facts 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

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

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

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

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

812 
(0 upto length facts  1 ~~ facts)), 
41157  813 
(class_relsN, map problem_line_for_class_rel_clause class_rel_clauses), 
814 
(aritiesN, map problem_line_for_arity_clause arity_clauses), 

815 
(helpersN, []), 

42533  816 
(type_declsN, []), 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

817 
(conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs), 
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

818 
(free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))] 
42520  819 
val sym_tab = sym_table_for_problem explicit_apply problem 
42521
02df3b78a438
get rid of "explicit_forall" proverspecific option, even if that means some clutter  foralls will be necessary to attach types to variables
blanchet
parents:
42520
diff
changeset

820 
val problem = problem > repair_problem thy type_sys sym_tab 
02df3b78a438
get rid of "explicit_forall" proverspecific option, even if that means some clutter  foralls will be necessary to attach types to variables
blanchet
parents:
42520
diff
changeset

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

822 
problem > maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi 
42528  823 
 _ => NONE) o snd) 
42527
6a9458524f01
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents:
42526
diff
changeset

824 
> get_helper_facts ctxt type_sys 
42533  825 
val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts) 
826 
val type_decl_lines = 

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

827 
Symtab.fold_rev (append o type_decl_lines_for_const ctxt type_sys sym_tab) 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

828 
const_tab [] 
41157  829 
val helper_lines = 
42521
02df3b78a438
get rid of "explicit_forall" proverspecific option, even if that means some clutter  foralls will be necessary to attach types to variables
blanchet
parents:
42520
diff
changeset

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

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

832 
#> problem_line_for_fact ctxt helper_prefix type_sys 
42521
02df3b78a438
get rid of "explicit_forall" proverspecific option, even if that means some clutter  foralls will be necessary to attach types to variables
blanchet
parents:
42520
diff
changeset

833 
#> repair_problem_line thy type_sys sym_tab) 
41157  834 
> op @ 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

835 
val (problem, pool) = 
42533  836 
problem > fold (AList.update (op =)) 
837 
[(helpersN, helper_lines), (type_declsN, type_decl_lines)] 

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

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

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

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

841 
case pool of SOME the_pool => snd the_pool  NONE => Symtab.empty, 
41157  842 
offset_of_heading_in_problem conjsN problem 0, 
843 
fact_names > Vector.fromList) 

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

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

845 

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

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

847 
val conj_weight = 0.0 
41770  848 
val hyp_weight = 0.1 
849 
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

850 
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

851 

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

852 
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

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

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

855 
fun add_problem_line_weights weight (Formula (_, _, _, phi, _, _)) = 
42528  856 
fold_formula (add_term_weights weight) phi 
857 
 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

858 

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

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

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

861 
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

862 
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

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

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

865 

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

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

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

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

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

870 
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

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

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

873 
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

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

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

876 

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

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

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

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

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

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

882 
> Symtab.dest 
41726  883 
> 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

884 

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

885 
end; 