author  blanchet 
Tue, 15 Nov 2011 22:13:39 +0100  
changeset 45510  96696c360b3e 
parent 45508  b216dc1b3630 
child 45511  9b0f8ca4388e 
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 
44411
e3629929b171
change Metis's default settings if type information axioms are generated
blanchet
parents:
44409
diff
changeset

12 
type type_enc = ATP_Translate.type_enc 
e3629929b171
change Metis's default settings if type information axioms are generated
blanchet
parents:
44409
diff
changeset

13 

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

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

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

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

17 

43094  18 
val metis_equal : string 
19 
val metis_predicator : string 

20 
val metis_app_op : string 

44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

21 
val metis_systematic_type_tag : string 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

22 
val metis_ad_hoc_type_tag : string 
42098
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset

23 
val metis_generated_var_prefix : string 
43231
69f22ac07395
nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents:
43224
diff
changeset

24 
val trace : bool Config.T 
69f22ac07395
nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents:
43224
diff
changeset

25 
val verbose : bool Config.T 
45508  26 
val lambda_translation : string Config.T 
43231
69f22ac07395
nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents:
43224
diff
changeset

27 
val trace_msg : Proof.context > (unit > string) > unit 
69f22ac07395
nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents:
43224
diff
changeset

28 
val verbose_warning : Proof.context > string > unit 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

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

30 
val reveal_old_skolem_terms : (string * term) list > term > term 
45508  31 
val reveal_lambda_lifted : (string * term) list > term > term 
40157  32 
val prepare_metis_problem : 
45508  33 
Proof.context > type_enc > string > thm list > thm list 
34 
> int Symtab.table * (Metis_Thm.thm * isa_thm) list 

35 
* ((string * term) list * (string * term) list) 

24310  36 
end 
15347  37 

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

38 
structure Metis_Translate : METIS_TRANSLATE = 
15347  39 
struct 
40 

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

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

42 
open ATP_Translate 
15347  43 

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

44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

46 
val metis_app_op = Metis_Name.toString Metis_Term.appName 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

47 
val metis_systematic_type_tag = 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

48 
Metis_Name.toString Metis_Term.hasTypeFunctionName 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

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

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

51 

43231
69f22ac07395
nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents:
43224
diff
changeset

52 
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false) 
69f22ac07395
nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents:
43224
diff
changeset

53 
val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true) 
45508  54 
val lambda_translation = 
55 
Attrib.setup_config_string @{binding metis_lambda_translation} 

56 
(K combinatorsN) 

43231
69f22ac07395
nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents:
43224
diff
changeset

57 

69f22ac07395
nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents:
43224
diff
changeset

58 
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () 
69f22ac07395
nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents:
43224
diff
changeset

59 
fun verbose_warning ctxt msg = 
69f22ac07395
nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents:
43224
diff
changeset

60 
if Config.get ctxt verbose then warning ("Metis: " ^ msg) else () 
69f22ac07395
nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents:
43224
diff
changeset

61 

43094  62 
val metis_name_table = 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

63 
[((tptp_equal, 2), (K metis_equal, false)), 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

64 
((tptp_old_equal, 2), (K metis_equal, false)), 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

65 
((prefixed_predicator_name, 1), (K metis_predicator, false)), 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

66 
((prefixed_app_op_name, 2), (K metis_app_op, false)), 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

67 
((prefixed_type_tag_name, 2), 
44782  68 
(fn type_enc => 
69 
if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag 

70 
else metis_ad_hoc_type_tag, true))] 

43094  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 
43826
2b094d17f432
fix subtle type inference bug in Metis  different occurrences of the same Skolem might need to be typed differently, using paramify_vars overconstraints the typing problem
blanchet
parents:
43626
diff
changeset

111 
> map_types (map_type_tvar (K dummyT)) 
37632  112 
else 
113 
t 

114 
 t => t) 

115 

45508  116 
fun reveal_lambda_lifted lambdas = 
117 
map_aterms (fn t as Free (s, _) => 

118 
if String.isPrefix lambda_lifted_prefix s then 

119 
case AList.lookup (op =) lambdas s of 

120 
SOME t => t > map_types (map_type_tvar (K dummyT)) 

121 
 NONE => t 

122 
else 

123 
t 

124 
 t => t) 

125 

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

126 

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

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

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

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

130 

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

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

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

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

134 

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

135 
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

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

137 
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

138 

44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

139 
fun metis_term_from_atp type_enc (ATerm (s, tms)) = 
43094  140 
if is_tptp_variable s then 
43268
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43259
diff
changeset

141 
Metis_Term.Var (Metis_Name.fromString s) 
43094  142 
else 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

143 
(case AList.lookup (op =) metis_name_table (s, length tms) of 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

144 
SOME (f, swap) => (f type_enc, swap) 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

145 
 NONE => (s, false)) 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

146 
> (fn (s, swap) => 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

147 
Metis_Term.Fn (Metis_Name.fromString s, 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

148 
tms > map (metis_term_from_atp type_enc) 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

149 
> swap ? rev)) 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

150 
fun metis_atom_from_atp type_enc (AAtom tm) = 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

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

152 
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

153 
 _ => raise Fail "non CNF  expected function") 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

154 
 metis_atom_from_atp _ _ = raise Fail "not CNF  expected atom" 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

155 
fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) = 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

156 
(false, metis_atom_from_atp type_enc phi) 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

157 
 metis_literal_from_atp type_enc phi = 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

158 
(true, metis_atom_from_atp type_enc phi) 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

159 
fun metis_literals_from_atp type_enc (AConn (AOr, phis)) = 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

160 
maps (metis_literals_from_atp type_enc) phis 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

161 
 metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi] 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

162 
fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) = 
43173  163 
let 
164 
fun some isa = 

44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

165 
SOME (phi > metis_literals_from_atp type_enc 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

166 
> Metis_LiteralSet.fromList 
43173  167 
> Metis_Thm.axiom, isa) 
168 
in 

169 
if ident = type_tag_idempotence_helper_name orelse 

44396
66b9b3fcd608
started cleaning up polymorphic monotonicitybased encodings, based on discussions with Nick Smallbone
blanchet
parents:
44394
diff
changeset

170 
String.isPrefix tags_sym_formula_prefix ident then 
43173  171 
Isa_Reflexive_or_Trivial > some 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

172 
else if String.isPrefix conjecture_prefix ident then 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

173 
NONE 
43173  174 
else if String.isPrefix helper_prefix ident then 
43194  175 
case (String.isSuffix typed_helper_suffix ident, 
176 
space_explode "_" ident) of 

177 
(needs_fairly_sound, _ :: const :: j :: _) => 

178 
nth ((const, needs_fairly_sound) 

179 
> AList.lookup (op =) helper_table > the) 

43173  180 
(the (Int.fromString j)  1) 
43194  181 
> prepare_helper 
182 
> Isa_Raw > some 

43173  183 
 _ => raise Fail ("malformed helper identifier " ^ quote ident) 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

184 
else case try (unprefix fact_prefix) ident of 
43173  185 
SOME s => 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

186 
let 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

187 
val j = s > space_explode "_" > List.last > Int.fromString > the 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

188 
in Meson.make_meta_clause (snd (nth clauses j)) > Isa_Raw > some end 
43173  189 
 NONE => TrueI > Isa_Raw > some 
190 
end 

44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

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

192 

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

193 
(* Function to generate metis clauses, including comb and type clauses *) 
45508  194 
fun prepare_metis_problem ctxt type_enc lambda_trans conj_clauses fact_clauses = 
43212  195 
let 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

196 
val (conj_clauses, fact_clauses) = 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43572
diff
changeset

197 
if polymorphism_of_type_enc type_enc = Polymorphic then 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

198 
(conj_clauses, fact_clauses) 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

199 
else 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

200 
conj_clauses @ fact_clauses 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

201 
> map (pair 0) 
45043
7e1a73fc0c8b
drop partial monomorphic instances in Metis, like in Sledgehammer
blanchet
parents:
45042
diff
changeset

202 
> rpair (ctxt > Config.put Monomorph.keep_partial_instances false) 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

203 
> Monomorph.monomorph atp_schematic_consts_of 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

204 
> fst > chop (length conj_clauses) 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

205 
> pairself (maps (map (zero_var_indexes o snd))) 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

206 
val num_conjs = length conj_clauses 
43212  207 
val clauses = 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

208 
map2 (fn j => pair (Int.toString j, Local)) 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

209 
(0 upto num_conjs  1) conj_clauses @ 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

210 
(* "General" below isn't quite correct; the fact could be local. *) 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

211 
map2 (fn j => pair (Int.toString (num_conjs + j), General)) 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

212 
(0 upto length fact_clauses  1) fact_clauses 
43212  213 
val (old_skolems, props) = 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

214 
fold_rev (fn (name, th) => fn (old_skolems, props) => 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

215 
th > prop_of > Logic.strip_imp_concl 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

216 
> conceal_old_skolem_terms (length clauses) old_skolems 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

217 
> (fn prop => (name, prop) :: props)) 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

218 
clauses ([], []) 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

219 
(* 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

220 
val _ = 
45042
89341b897412
better type reconstruction  prevents illinstantiations in proof replay
blanchet
parents:
44782
diff
changeset

221 
tracing ("PROPS:\n" ^ 
89341b897412
better type reconstruction  prevents illinstantiations in proof replay
blanchet
parents:
44782
diff
changeset

222 
cat_lines (map (Syntax.string_of_term ctxt o snd) props)) 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

223 
*) 
45508  224 
val (lambda_trans, preproc) = 
225 
if lambda_trans = combinatorsN then (no_lambdasN, false) 

226 
else (lambda_trans, true) 

227 
val (atp_problem, _, _, _, _, _, lifted, sym_tab) = 

228 
prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans 

229 
false preproc [] @{prop False} props 

45510  230 
(* 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43268
diff
changeset

231 
val _ = tracing ("ATP PROBLEM: " ^ 
45508  232 
cat_lines (lines_for_atp_problem CNF atp_problem)) 
45510  233 
*) 
45508  234 
(* "rev" is for compatibility with existing proof scripts. *) 
43212  235 
val axioms = 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

236 
atp_problem 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

237 
> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) > rev 
45508  238 
in (sym_tab, axioms, (lifted, old_skolems)) end 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

239 

15347  240 
end; 