author  blanchet 
Mon, 06 Jun 2011 20:36:35 +0200  
changeset 43175  4ca344fe0aca 
parent 43174  f497a1e97d37 
child 43180  283114859d6c 
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 

43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

17 
datatype isa_thm = 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

18 
Isa_Reflexive_or_Trivial  
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

19 
Isa_Raw of thm 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

20 

40157  21 
type metis_problem = 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

22 
{axioms : (Metis_Thm.thm * isa_thm) list, 
43094  23 
tfrees : type_literal list, 
24 
old_skolems : (string * term) list} 

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

25 

43094  26 
val metis_equal : string 
27 
val metis_predicator : string 

28 
val metis_app_op : string 

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

30 
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

31 
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

32 
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

33 
val string_of_mode : mode > string 
40157  34 
val prepare_metis_problem : 
43102  35 
Proof.context > mode > type_sys option > thm list > thm list 
43094  36 
> mode * int Symtab.table * metis_problem 
24310  37 
end 
15347  38 

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

39 
structure Metis_Translate : METIS_TRANSLATE = 
15347  40 
struct 
41 

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

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

43 
open ATP_Translate 
15347  44 

43094  45 
val metis_equal = "=" 
46 
val metis_predicator = "{}" 

47 
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

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

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

50 

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

52 
[((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

53 
((tptp_old_equal, 2), (metis_equal, false)), 
43174  54 
((prefixed_predicator_name, 1), (metis_predicator, false)), 
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset

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

56 
((prefixed_type_tag_name, 2), (metis_type_tag, true))] 
43094  57 

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

58 
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

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

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

61 

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

62 
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

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

64 
 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

65 
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

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

67 
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

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

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

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

71 

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

72 
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

73 
old_skolem_const_prefix ^ Long_Name.separator ^ 
41491  74 
(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

75 

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

76 
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

77 
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

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

79 
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

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

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

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

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

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

85 
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

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

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

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

89 
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

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

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

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

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

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

95 
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

96 
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

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

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

99 
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

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

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

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

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

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

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

106 

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

107 
fun reveal_old_skolem_terms old_skolems = 
37632  108 
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

109 
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

110 
AList.lookup (op =) old_skolems s > the 
37632  111 
> map_types Type_Infer.paramify_vars 
112 
else 

113 
t 

114 
 t => t) 

115 

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

116 

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

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

118 
(* HOL to FOL (Isabelle to Metis) *) 
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 

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

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

123 

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

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

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

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

128 

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

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

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

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

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

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

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

135 
 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

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

137 

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

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

140 

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

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

142 

42562  143 
fun metis_term_from_typ (Type (s, Ts)) = 
144 
Metis_Term.Fn (make_fixed_type_const s, map metis_term_from_typ Ts) 

145 
 metis_term_from_typ (TFree (s, _)) = 

146 
Metis_Term.Fn (make_fixed_type_var s, []) 

147 
 metis_term_from_typ (TVar (x, _)) = 

148 
Metis_Term.Var (make_schematic_type_var x) 

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

149 

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

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

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

152 

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

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

154 
case strip_combterm_comb tm of 
42562  155 
(CombConst ((c, _), _, Ts), tms) => 
156 
let val tyargs = map metis_term_from_typ Ts 

157 
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

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

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

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

161 

42562  162 
fun hol_term_to_fol_HO (CombConst ((a, _), _, Ts)) = 
43094  163 
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

164 
 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

165 
 hol_term_to_fol_HO (CombApp (tm1, tm2)) = 
43094  166 
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

167 

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

168 
(*The fullytyped translation, to avoid type errors*) 
42562  169 
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

170 
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

171 

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

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

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

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

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

176 
 hol_term_to_fol_FT (tm as CombApp (tm1,tm2)) = 
43094  177 
tag_with_type 
178 
(Metis_Term.Fn (metis_app_op, map hol_term_to_fol_FT [tm1, tm2])) 

179 
(combtyp_of tm) 

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

180 

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

181 
fun hol_literal_to_fol FO (pos, tm) = 
42562  182 
let 
183 
val (CombConst((p, _), _, Ts), tms) = strip_combterm_comb tm 

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

185 
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

186 
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

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

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

189 
(CombConst(("equal", _), _, _), tms) => 
43094  190 
metis_lit pos metis_equal (map hol_term_to_fol_HO tms) 
191 
 _ => 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

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

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

194 
(CombConst(("equal", _), _, _), tms) => 
43094  195 
metis_lit pos metis_equal (map hol_term_to_fol_FT tms) 
196 
 _ => 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

197 

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

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

199 
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

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

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

202 

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

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

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

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

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

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

208 

42352  209 
fun has_default_sort _ (TVar _) = false 
210 
 has_default_sort ctxt (TFree (x, s)) = 

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

212 

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

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

214 
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

215 

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

217 
let 
42361  218 
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

219 
val (old_skolems, (mlits, types_sorts)) = 
39888  220 
th > prop_of > Logic.strip_imp_concl 
221 
> conceal_old_skolem_terms j old_skolems 

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

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

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

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

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

226 
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

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

228 
let 
42352  229 
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

230 
> raw_type_literals_for_types 
43090  231 
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

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

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

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

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

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

237 

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

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

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

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

241 

43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

242 
datatype isa_thm = 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

243 
Isa_Reflexive_or_Trivial  
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

244 
Isa_Raw of thm 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

245 

40157  246 
type metis_problem = 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

247 
{axioms : (Metis_Thm.thm * isa_thm) list, 
43094  248 
tfrees : type_literal list, 
249 
old_skolems : (string * term) list} 

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

250 

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

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

252 
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

253 

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

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

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

256 
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

257 
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

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

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

260 

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

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

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

263 
fun in_mterm (Metis_Term.Var _) = false 
41156  264 
 in_mterm (Metis_Term.Fn (nm, tm_list)) = 
265 
c = nm orelse exists in_mterm tm_list 

266 
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

267 

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

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

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

270 
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

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

272 
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

273 
(* TrueI is returned as the Isabelle counterpart because there isn't any. *) 
43086  274 
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

275 
(TrueI, 
42895  276 
Metis_Thm.axiom (Metis_LiteralSet.fromList 
277 
(map m_arity_cls (concl_lits :: prem_lits)))); 

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 
(* CLASSREL CLAUSE *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

280 
fun m_class_rel_cls (subclass, _) (superclass, _) = 
43091  281 
[metis_lit false subclass [Metis_Term.Var "T"], 
282 
metis_lit true superclass [Metis_Term.Var "T"]] 

43086  283 
fun class_rel_cls ({subclass, superclass, ...} : class_rel_clause) = 
43091  284 
(TrueI, m_class_rel_cls subclass superclass 
285 
> Metis_LiteralSet.fromList > Metis_Thm.axiom) 

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

286 

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

287 
fun type_ext thy tms = 
43091  288 
let 
289 
val subs = tfree_classes_of_terms tms 

290 
val supers = tvar_classes_of_terms tms 

291 
val tycons = type_consts_of_terms thy tms 

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

293 
val class_rel_clauses = make_class_rel_clauses thy subs supers' 

294 
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

295 

43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

296 
val proxy_defs = map (fst o snd o snd) proxy_table 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

297 
val prepare_helper = 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

298 
Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs) 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

299 

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

301 
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

302 
fun metis_term_from_atp (ATerm (s, tms)) = 
43094  303 
if is_tptp_variable s then 
304 
Metis_Term.Var s 

305 
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

306 
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

307 
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

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

309 
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

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

311 
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

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

313 
 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

314 
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

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

316 
 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

317 
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

318 
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

319 
 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

320 
fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) = 
43173  321 
let 
322 
fun some isa = 

323 
SOME (phi > metis_literals_from_atp > Metis_LiteralSet.fromList 

324 
> Metis_Thm.axiom, isa) 

325 
in 

326 
if ident = type_tag_idempotence_helper_name orelse 

327 
String.isPrefix lightweight_tags_sym_formula_prefix ident then 

328 
Isa_Reflexive_or_Trivial > some 

329 
else if String.isPrefix helper_prefix ident then 

330 
case space_explode "_" ident of 

331 
_ :: const :: j :: _ => 

43175
4ca344fe0aca
properly locate helpers whose constants have several entries in the helper table
blanchet
parents:
43174
diff
changeset

332 
nth (helper_table > filter (curry (op =) const o fst) 
4ca344fe0aca
properly locate helpers whose constants have several entries in the helper table
blanchet
parents:
43174
diff
changeset

333 
> maps (snd o snd)) 
43173  334 
(the (Int.fromString j)  1) 
335 
> prepare_helper > Isa_Raw > some 

336 
 _ => raise Fail ("malformed helper identifier " ^ quote ident) 

337 
else case try (unprefix conjecture_prefix) ident of 

338 
SOME s => 

339 
let val j = the (Int.fromString s) in 

340 
if j = length clauses then NONE 

341 
else Meson.make_meta_clause (nth clauses j) > Isa_Raw > some 

342 
end 

343 
 NONE => TrueI > Isa_Raw > some 

344 
end 

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

345 
 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

346 

43128  347 
val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight) 
43100  348 

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

349 
(* Function to generate metis clauses, including comb and type clauses *) 
43103  350 
fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses = 
43091  351 
let 
43100  352 
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

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

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

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

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

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

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

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

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

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

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

364 
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

365 
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

366 
val axioms = 
43173  367 
atp_problem > maps (map_filter (metis_axiom_from_atp clauses) o snd) 
43094  368 
in 
43103  369 
(MX, sym_tab, 
43094  370 
{axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)}) 
371 
end 

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

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

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

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

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

377 
if mode = HO andalso 
43091  378 
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

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

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

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

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

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

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

386 
val (mth, tfree_lits, old_skolems) = 
43090  387 
hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems 
388 
metis_ith 

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

389 
in 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

390 
{axioms = (mth, Isa_Raw isa_ith) :: axioms, 
43091  391 
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

392 
end; 
43091  393 
fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} = 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

394 
{axioms = (mth, Isa_Raw ith) :: axioms, tfrees = tfrees, 
43091  395 
old_skolems = old_skolems} 
396 
fun add_tfrees {axioms, tfrees, old_skolems} = 

43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

397 
{axioms = map (rpair (Isa_Raw TrueI) o metis_of_tfree) 
43129  398 
(distinct (op =) tfrees) @ axioms, 
43091  399 
tfrees = tfrees, old_skolems = old_skolems} 
400 
val problem = 

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

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

403 
> add_tfrees 

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

404 
> fold (add_thm false o `Meson.make_meta_clause) fact_clauses 
43091  405 
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

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

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

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

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

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

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

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

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

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

417 
if needs_full_types andalso mode <> FT then [] 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset

418 
else map (`prepare_helper) thms) 
43091  419 
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

420 
val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses)) 
43094  421 
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

422 

15347  423 
end; 