author  blanchet 
Wed, 01 Jun 2011 10:29:43 +0200  
changeset 43132  44cd26bfc30c 
parent 43130  d73fc2e55308 
child 43159  29b55f292e0b 
permissions  rwrr 
39958  1 
(* Title: HOL/Tools/Metis/metis_translate.ML 
38027  2 
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

3 
Author: Kong W. Susanto, Cambridge University Computer Laboratory 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

4 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36378
diff
changeset

5 
Author: Jasmin Blanchette, TU Muenchen 
15347  6 

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

7 
Translation of HOL to FOL for Metis. 
15347  8 
*) 
9 

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

10 
signature METIS_TRANSLATE = 
24310  11 
sig 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

12 
type type_literal = ATP_Translate.type_literal 
43102  13 
type type_sys = ATP_Translate.type_sys 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

14 

43103  15 
datatype mode = FO  HO  FT  MX 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

16 

40157  17 
type metis_problem = 
43129  18 
{axioms : (Metis_Thm.thm * thm option) list, 
43094  19 
tfrees : type_literal list, 
20 
old_skolems : (string * term) list} 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

21 

43094  22 
val metis_equal : string 
23 
val metis_predicator : string 

24 
val metis_app_op : string 

43106  25 
val metis_type_tag : string 
42098
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset

26 
val metis_generated_var_prefix : string 
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

27 
val metis_name_table : ((string * int) * (string * bool)) list 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

28 
val reveal_old_skolem_terms : (string * term) list > term > term 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

29 
val string_of_mode : mode > string 
40157  30 
val prepare_metis_problem : 
43102  31 
Proof.context > mode > type_sys option > thm list > thm list 
43094  32 
> mode * int Symtab.table * metis_problem 
24310  33 
end 
15347  34 

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

35 
structure Metis_Translate : METIS_TRANSLATE = 
15347  36 
struct 
37 

43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

38 
open ATP_Problem 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

39 
open ATP_Translate 
15347  40 

43094  41 
val metis_equal = "=" 
42 
val metis_predicator = "{}" 

43 
val metis_app_op = "." 

43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

44 
val metis_type_tag = ":" 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

45 
val metis_generated_var_prefix = "_" 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

46 

43094  47 
val metis_name_table = 
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

48 
[((tptp_equal, 2), (metis_equal, false)), 
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

49 
((tptp_old_equal, 2), (metis_equal, false)), 
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

50 
((const_prefix ^ predicator_name, 1), (metis_predicator, false)), 
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset

51 
((prefixed_app_op_name, 2), (metis_app_op, false)), 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset

52 
((prefixed_type_tag_name, 2), (metis_type_tag, true))] 
43094  53 

40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

54 
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

55 
 predicate_of thy (t, pos) = 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

56 
(combterm_from_term thy [] (Envir.eta_contract t), pos) 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

57 

40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

58 
fun literals_of_term1 args thy (@{const Trueprop} $ P) = 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

59 
literals_of_term1 args thy P 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

60 
 literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) = 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

61 
literals_of_term1 (literals_of_term1 args thy P) thy Q 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

62 
 literals_of_term1 (lits, ts) thy P = 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

63 
let val ((pred, ts'), pol) = predicate_of thy (P, true) in 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

64 
((pol, pred) :: lits, union (op =) ts ts') 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

65 
end 
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

66 
val literals_of_term = literals_of_term1 ([], []) 
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

67 

39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset

68 
fun old_skolem_const_name i j num_T_args = 
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset

69 
old_skolem_const_prefix ^ Long_Name.separator ^ 
41491  70 
(space_implode Long_Name.separator (map string_of_int [i, j, num_T_args])) 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

71 

39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

72 
fun conceal_old_skolem_terms i old_skolems t = 
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39946
diff
changeset

73 
if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

74 
let 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

75 
fun aux old_skolems 
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39946
diff
changeset

76 
(t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) = 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

77 
let 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

78 
val (old_skolems, s) = 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

79 
if i = ~1 then 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

80 
(old_skolems, @{const_name undefined}) 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

81 
else case AList.find (op aconv) old_skolems t of 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

82 
s :: _ => (old_skolems, s) 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

83 
 [] => 
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

84 
let 
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset

85 
val s = old_skolem_const_name i (length old_skolems) 
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset

86 
(length (Term.add_tvarsT T [])) 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

87 
in ((s, t) :: old_skolems, s) end 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

88 
in (old_skolems, Const (s, T)) end 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

89 
 aux old_skolems (t1 $ t2) = 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

90 
let 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

91 
val (old_skolems, t1) = aux old_skolems t1 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

92 
val (old_skolems, t2) = aux old_skolems t2 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

93 
in (old_skolems, t1 $ t2) end 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

94 
 aux old_skolems (Abs (s, T, t')) = 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

95 
let val (old_skolems, t') = aux old_skolems t' in 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

96 
(old_skolems, Abs (s, T, t')) 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

97 
end 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

98 
 aux old_skolems t = (old_skolems, t) 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

99 
in aux old_skolems t end 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

100 
else 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

101 
(old_skolems, t) 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

102 

39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

103 
fun reveal_old_skolem_terms old_skolems = 
37632  104 
map_aterms (fn t as Const (s, _) => 
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset

105 
if String.isPrefix old_skolem_const_prefix s then 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

106 
AList.lookup (op =) old_skolems s > the 
37632  107 
> map_types Type_Infer.paramify_vars 
108 
else 

109 
t 

110 
 t => t) 

111 

37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

112 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

113 
(*  *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

114 
(* HOL to FOL (Isabelle to Metis) *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

115 
(*  *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

116 

43103  117 
(* firstorder, higherorder, fullytyped, mode X (fleXible) *) 
118 
datatype mode = FO  HO  FT  MX 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

119 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

120 
fun string_of_mode FO = "FO" 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

121 
 string_of_mode HO = "HO" 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

122 
 string_of_mode FT = "FT" 
43103  123 
 string_of_mode MX = "MX" 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

124 

42745
b817c6f91a98
reenabled equality proxy in Metis for higherorder reasoning
blanchet
parents:
42727
diff
changeset

125 
fun fn_isa_to_met_sublevel "equal" = "c_fequal" 
41139
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

126 
 fn_isa_to_met_sublevel "c_False" = "c_fFalse" 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

127 
 fn_isa_to_met_sublevel "c_True" = "c_fTrue" 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

128 
 fn_isa_to_met_sublevel "c_Not" = "c_fNot" 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

129 
 fn_isa_to_met_sublevel "c_conj" = "c_fconj" 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

130 
 fn_isa_to_met_sublevel "c_disj" = "c_fdisj" 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

131 
 fn_isa_to_met_sublevel "c_implies" = "c_fimplies" 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

132 
 fn_isa_to_met_sublevel x = x 
42758
865ce93ce025
handle equality proxy in a more backwardcompatible way
blanchet
parents:
42745
diff
changeset

133 

43094  134 
fun fn_isa_to_met_toplevel "equal" = metis_equal 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

135 
 fn_isa_to_met_toplevel x = x 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

136 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

137 
fun metis_lit b c args = (b, (c, args)); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

138 

42562  139 
fun metis_term_from_typ (Type (s, Ts)) = 
140 
Metis_Term.Fn (make_fixed_type_const s, map metis_term_from_typ Ts) 

141 
 metis_term_from_typ (TFree (s, _)) = 

142 
Metis_Term.Fn (make_fixed_type_var s, []) 

143 
 metis_term_from_typ (TVar (x, _)) = 

144 
Metis_Term.Var (make_schematic_type_var x) 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

145 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

146 
(*These two functions insert type literals before the real literals. That is the 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

147 
opposite order from TPTP linkup, but maybe OK.*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

148 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

149 
fun hol_term_to_fol_FO tm = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

150 
case strip_combterm_comb tm of 
42562  151 
(CombConst ((c, _), _, Ts), tms) => 
152 
let val tyargs = map metis_term_from_typ Ts 

153 
val args = map hol_term_to_fol_FO tms 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

154 
in Metis_Term.Fn (c, tyargs @ args) end 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

155 
 (CombVar ((v, _), _), []) => Metis_Term.Var v 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

156 
 _ => raise Fail "nonfirstorder combterm" 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

157 

42562  158 
fun hol_term_to_fol_HO (CombConst ((a, _), _, Ts)) = 
43094  159 
Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_typ Ts) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

160 
 hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

161 
 hol_term_to_fol_HO (CombApp (tm1, tm2)) = 
43094  162 
Metis_Term.Fn (metis_app_op, map hol_term_to_fol_HO [tm1, tm2]) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

163 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

164 
(*The fullytyped translation, to avoid type errors*) 
42562  165 
fun tag_with_type tm T = 
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

166 
Metis_Term.Fn (metis_type_tag, [tm, metis_term_from_typ T]) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

167 

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

168 
fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
40259
diff
changeset

169 
tag_with_type (Metis_Term.Var s) ty 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
40259
diff
changeset

170 
 hol_term_to_fol_FT (CombConst ((a, _), ty, _)) = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
40259
diff
changeset

171 
tag_with_type (Metis_Term.Fn (fn_isa_to_met_sublevel a, [])) ty 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
40259
diff
changeset

172 
 hol_term_to_fol_FT (tm as CombApp (tm1,tm2)) = 
43094  173 
tag_with_type 
174 
(Metis_Term.Fn (metis_app_op, map hol_term_to_fol_FT [tm1, tm2])) 

175 
(combtyp_of tm) 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

176 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

177 
fun hol_literal_to_fol FO (pos, tm) = 
42562  178 
let 
179 
val (CombConst((p, _), _, Ts), tms) = strip_combterm_comb tm 

180 
val tylits = if p = "equal" then [] else map metis_term_from_typ Ts 

181 
val lits = map hol_term_to_fol_FO tms 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

182 
in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

183 
 hol_literal_to_fol HO (pos, tm) = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

184 
(case strip_combterm_comb tm of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

185 
(CombConst(("equal", _), _, _), tms) => 
43094  186 
metis_lit pos metis_equal (map hol_term_to_fol_HO tms) 
187 
 _ => metis_lit pos metis_predicator [hol_term_to_fol_HO tm]) 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

188 
 hol_literal_to_fol FT (pos, tm) = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

189 
(case strip_combterm_comb tm of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

190 
(CombConst(("equal", _), _, _), tms) => 
43094  191 
metis_lit pos metis_equal (map hol_term_to_fol_FT tms) 
192 
 _ => metis_lit pos metis_predicator [hol_term_to_fol_FT tm]) 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

193 

40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

194 
fun literals_of_hol_term thy mode t = 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

195 
let val (lits, types_sorts) = literals_of_term thy t in 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

196 
(map (hol_literal_to_fol mode) lits, types_sorts) 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

197 
end 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

198 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

199 
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

200 
fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

201 
metis_lit pos s [Metis_Term.Var s'] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

202 
 metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

203 
metis_lit pos s [Metis_Term.Fn (s',[])] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

204 

42352  205 
fun has_default_sort _ (TVar _) = false 
206 
 has_default_sort ctxt (TFree (x, s)) = 

207 
(s = the_default [] (Variable.def_sort ctxt (x, ~1))); 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

208 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

209 
fun metis_of_tfree tf = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

210 
Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf)); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

211 

43090  212 
fun hol_thm_to_fol is_conjecture ctxt mode j old_skolems th = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

213 
let 
42361  214 
val thy = Proof_Context.theory_of ctxt 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

215 
val (old_skolems, (mlits, types_sorts)) = 
39888  216 
th > prop_of > Logic.strip_imp_concl 
217 
> conceal_old_skolem_terms j old_skolems 

40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

218 
> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

219 
in 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

220 
if is_conjecture then 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

221 
(Metis_Thm.axiom (Metis_LiteralSet.fromList mlits), 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

222 
raw_type_literals_for_types types_sorts, old_skolems) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

223 
else 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

224 
let 
42352  225 
val tylits = types_sorts > filter_out (has_default_sort ctxt) 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

226 
> raw_type_literals_for_types 
43090  227 
val mtylits = map (metis_of_type_literals false) tylits 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

228 
in 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

229 
(Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [], 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

230 
old_skolems) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

231 
end 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

232 
end; 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

233 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

234 
(*  *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

235 
(* Logic maps manage the interface between HOL and firstorder logic. *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

236 
(*  *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

237 

40157  238 
type metis_problem = 
43129  239 
{axioms : (Metis_Thm.thm * thm option) list, 
43094  240 
tfrees : type_literal list, 
241 
old_skolems : (string * term) list} 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

242 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

243 
fun is_quasi_fol_clause thy = 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

244 
Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

245 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

246 
(*Extract TFree constraints from context to include as conjecture clauses*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

247 
fun init_tfrees ctxt = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

248 
let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

249 
Vartab.fold add (#2 (Variable.constraints_of ctxt)) [] 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

250 
> raw_type_literals_for_types 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

251 
end; 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

252 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

253 
fun const_in_metis c (pred, tm_list) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

254 
let 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

255 
fun in_mterm (Metis_Term.Var _) = false 
41156  256 
 in_mterm (Metis_Term.Fn (nm, tm_list)) = 
257 
c = nm orelse exists in_mterm tm_list 

258 
in c = pred orelse exists in_mterm tm_list end 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

259 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

260 
(* ARITY CLAUSE *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

261 
fun m_arity_cls (TConsLit ((c, _), (t, _), args)) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

262 
metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

263 
 m_arity_cls (TVarLit ((c, _), (s, _))) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

264 
metis_lit false c [Metis_Term.Var s] 
43125
ddf63baabdec
distinguish different kinds of typing informations in the fact name
blanchet
parents:
43109
diff
changeset

265 
(* TrueI is returned as the Isabelle counterpart because there isn't any. *) 
43086  266 
fun arity_cls ({prem_lits, concl_lits, ...} : arity_clause) = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

267 
(TrueI, 
42895  268 
Metis_Thm.axiom (Metis_LiteralSet.fromList 
269 
(map m_arity_cls (concl_lits :: prem_lits)))); 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

270 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

271 
(* CLASSREL CLAUSE *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

272 
fun m_class_rel_cls (subclass, _) (superclass, _) = 
43091  273 
[metis_lit false subclass [Metis_Term.Var "T"], 
274 
metis_lit true superclass [Metis_Term.Var "T"]] 

43086  275 
fun class_rel_cls ({subclass, superclass, ...} : class_rel_clause) = 
43091  276 
(TrueI, m_class_rel_cls subclass superclass 
277 
> Metis_LiteralSet.fromList > Metis_Thm.axiom) 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

278 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

279 
fun type_ext thy tms = 
43091  280 
let 
281 
val subs = tfree_classes_of_terms tms 

282 
val supers = tvar_classes_of_terms tms 

283 
val tycons = type_consts_of_terms thy tms 

284 
val (supers', arity_clauses) = make_arity_clauses thy tycons supers 

285 
val class_rel_clauses = make_class_rel_clauses thy subs supers' 

286 
in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

287 

43094  288 
fun metis_name_from_atp s ary = 
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

289 
AList.lookup (op =) metis_name_table (s, ary) > the_default (s, false) 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

290 
fun metis_term_from_atp (ATerm (s, tms)) = 
43094  291 
if is_tptp_variable s then 
292 
Metis_Term.Var s 

293 
else 

43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

294 
let val (s, swap) = metis_name_from_atp s (length tms) in 
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

295 
Metis_Term.Fn (s, tms > map metis_term_from_atp > swap ? rev) 
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

296 
end 
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

297 
fun metis_atom_from_atp (AAtom tm) = 
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

298 
(case metis_term_from_atp tm of 
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

299 
Metis_Term.Fn x => x 
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

300 
 _ => raise Fail "non CNF  expected function") 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

301 
 metis_atom_from_atp _ = raise Fail "not CNF  expected atom" 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

302 
fun metis_literal_from_atp (AConn (ANot, [phi])) = 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

303 
(false, metis_atom_from_atp phi) 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

304 
 metis_literal_from_atp phi = (true, metis_atom_from_atp phi) 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

305 
fun metis_literals_from_atp (AConn (AOr, [phi1, phi2])) = 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

306 
uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2)) 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

307 
 metis_literals_from_atp phi = [metis_literal_from_atp phi] 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

308 
fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) = 
43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

309 
(phi > metis_literals_from_atp > Metis_LiteralSet.fromList 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

310 
> Metis_Thm.axiom, 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

311 
case try (unprefix conjecture_prefix) ident of 
43129  312 
SOME s => 
313 
SOME (Meson.make_meta_clause (nth clauses (the (Int.fromString s)))) 

43128  314 
 NONE => 
43129  315 
if String.isPrefix lightweight_tags_sym_formula_prefix ident then 
316 
NONE 

43128  317 
(* FIXME: missing: 
43129  318 
else if String.isPrefix helper_prefix then 
43128  319 
... 
43129  320 
*) 
43128  321 
else 
43129  322 
SOME TrueI) 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

323 
 metis_axiom_from_atp _ _ = raise Fail "not CNF  expected formula" 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

324 

43128  325 
val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight) 
43100  326 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

327 
(* Function to generate metis clauses, including comb and type clauses *) 
43103  328 
fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses = 
43091  329 
let 
43100  330 
val type_sys = type_sys > the_default default_type_sys 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

331 
val explicit_apply = NONE 
43109
8c9046951dcb
monomorphize in the new Metis if the type system calls for it
blanchet
parents:
43106
diff
changeset

332 
val clauses = 
8c9046951dcb
monomorphize in the new Metis if the type system calls for it
blanchet
parents:
43106
diff
changeset

333 
conj_clauses @ fact_clauses 
8c9046951dcb
monomorphize in the new Metis if the type system calls for it
blanchet
parents:
43106
diff
changeset

334 
> (if polymorphism_of_type_sys type_sys = Polymorphic then 
8c9046951dcb
monomorphize in the new Metis if the type system calls for it
blanchet
parents:
43106
diff
changeset

335 
I 
8c9046951dcb
monomorphize in the new Metis if the type system calls for it
blanchet
parents:
43106
diff
changeset

336 
else 
8c9046951dcb
monomorphize in the new Metis if the type system calls for it
blanchet
parents:
43106
diff
changeset

337 
map (pair 0) 
8c9046951dcb
monomorphize in the new Metis if the type system calls for it
blanchet
parents:
43106
diff
changeset

338 
#> rpair ctxt 
8c9046951dcb
monomorphize in the new Metis if the type system calls for it
blanchet
parents:
43106
diff
changeset

339 
#> Monomorph.monomorph Monomorph.all_schematic_consts_of 
43132
44cd26bfc30c
ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on
blanchet
parents:
43130
diff
changeset

340 
#> fst #> maps (map (zero_var_indexes o snd))) 
43094  341 
val (atp_problem, _, _, _, _, _, sym_tab) = 
43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

342 
prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

343 
false false (map prop_of clauses) @{prop False} [] 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

344 
val axioms = 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

345 
atp_problem 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

346 
> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd) 
43094  347 
in 
43103  348 
(MX, sym_tab, 
43094  349 
{axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)}) 
350 
end 

43100  351 
 prepare_metis_problem ctxt mode _ conj_clauses fact_clauses = 
43087
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

352 
let 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

353 
val thy = Proof_Context.theory_of ctxt 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

354 
(* The modes FO and FT are sticky. HO can be downgraded to FO. *) 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

355 
val mode = 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

356 
if mode = HO andalso 
43091  357 
forall (forall (is_quasi_fol_clause thy)) 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

358 
[conj_clauses, fact_clauses] then 
43087
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

359 
FO 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

360 
else 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

361 
mode 
41139
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

362 
fun add_thm is_conjecture (isa_ith, metis_ith) 
40157  363 
{axioms, tfrees, old_skolems} : metis_problem = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

364 
let 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

365 
val (mth, tfree_lits, old_skolems) = 
43090  366 
hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems 
367 
metis_ith 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

368 
in 
43129  369 
{axioms = (mth, SOME isa_ith) :: axioms, 
43091  370 
tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems} 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

371 
end; 
43091  372 
fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} = 
43129  373 
{axioms = (mth, SOME ith) :: axioms, tfrees = tfrees, 
43091  374 
old_skolems = old_skolems} 
375 
fun add_tfrees {axioms, tfrees, old_skolems} = 

43129  376 
{axioms = map (rpair (SOME TrueI) o metis_of_tfree) 
377 
(distinct (op =) tfrees) @ axioms, 

43091  378 
tfrees = tfrees, old_skolems = old_skolems} 
379 
val problem = 

380 
{axioms = [], tfrees = init_tfrees ctxt, old_skolems = []} 

381 
> fold (add_thm true o `Meson.make_meta_clause) conj_clauses 

382 
> add_tfrees 

43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

383 
> fold (add_thm false o `Meson.make_meta_clause) fact_clauses 
43091  384 
val clause_lists = map (Metis_Thm.clause o #1) (#axioms problem) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

385 
fun is_used c = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

386 
exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists 
43091  387 
val problem = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

388 
if mode = FO then 
43091  389 
problem 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

390 
else 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

391 
let 
41156  392 
val fdefs = @{thms fFalse_def fTrue_def fNot_def fconj_def fdisj_def 
393 
fimplies_def fequal_def} 

41139
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

394 
val prepare_helper = 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

395 
zero_var_indexes 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

396 
#> `(Meson.make_meta_clause 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

397 
#> rewrite_rule (map safe_mk_meta_eq fdefs)) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

398 
val helper_ths = 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

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

400 
> filter (is_used o prefix const_prefix o fst) 
42894
ce269ee43800
further improvements to "poly_{preds,tags}_{bang,query}"  better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents:
42893
diff
changeset

401 
> maps (fn (_, (needs_full_types, thms)) => 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41139
diff
changeset

402 
if needs_full_types andalso mode <> FT then [] 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41139
diff
changeset

403 
else map prepare_helper thms) 
43091  404 
in problem > fold (add_thm false) helper_ths end 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

405 
val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses)) 
43094  406 
in (mode, Symtab.empty, fold add_type_thm type_ths problem) end 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

407 

15347  408 
end; 