1 (* Title: HOL/Tools/Metis/metis_translate.ML |
|
2 Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
|
3 Author: Kong W. Susanto, Cambridge University Computer Laboratory |
|
4 Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
|
5 Author: Jasmin Blanchette, TU Muenchen |
|
6 |
|
7 Translation of HOL to FOL for Metis. |
|
8 *) |
|
9 |
|
10 signature METIS_TRANSLATE = |
|
11 sig |
|
12 type type_enc = ATP_Translate.type_enc |
|
13 |
|
14 datatype isa_thm = |
|
15 Isa_Reflexive_or_Trivial | |
|
16 Isa_Lambda_Lifted | |
|
17 Isa_Raw of thm |
|
18 |
|
19 val metis_equal : string |
|
20 val metis_predicator : string |
|
21 val metis_app_op : string |
|
22 val metis_systematic_type_tag : string |
|
23 val metis_ad_hoc_type_tag : string |
|
24 val metis_generated_var_prefix : string |
|
25 val trace : bool Config.T |
|
26 val verbose : bool Config.T |
|
27 val trace_msg : Proof.context -> (unit -> string) -> unit |
|
28 val verbose_warning : Proof.context -> string -> unit |
|
29 val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list |
|
30 val reveal_old_skolem_terms : (string * term) list -> term -> term |
|
31 val reveal_lam_lifted : (string * term) list -> term -> term |
|
32 val prepare_metis_problem : |
|
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) |
|
36 end |
|
37 |
|
38 structure Metis_Translate : METIS_TRANSLATE = |
|
39 struct |
|
40 |
|
41 open ATP_Problem |
|
42 open ATP_Translate |
|
43 |
|
44 val metis_equal = "=" |
|
45 val metis_predicator = "{}" |
|
46 val metis_app_op = Metis_Name.toString Metis_Term.appName |
|
47 val metis_systematic_type_tag = |
|
48 Metis_Name.toString Metis_Term.hasTypeFunctionName |
|
49 val metis_ad_hoc_type_tag = "**" |
|
50 val metis_generated_var_prefix = "_" |
|
51 |
|
52 val trace = Attrib.setup_config_bool @{binding metis_trace} (K false) |
|
53 val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true) |
|
54 |
|
55 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () |
|
56 fun verbose_warning ctxt msg = |
|
57 if Config.get ctxt verbose then warning ("Metis: " ^ msg) else () |
|
58 |
|
59 val metis_name_table = |
|
60 [((tptp_equal, 2), (K metis_equal, false)), |
|
61 ((tptp_old_equal, 2), (K metis_equal, false)), |
|
62 ((prefixed_predicator_name, 1), (K metis_predicator, false)), |
|
63 ((prefixed_app_op_name, 2), (K metis_app_op, false)), |
|
64 ((prefixed_type_tag_name, 2), |
|
65 (fn type_enc => |
|
66 if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag |
|
67 else metis_ad_hoc_type_tag, true))] |
|
68 |
|
69 fun old_skolem_const_name i j num_T_args = |
|
70 old_skolem_const_prefix ^ Long_Name.separator ^ |
|
71 (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args])) |
|
72 |
|
73 fun conceal_old_skolem_terms i old_skolems t = |
|
74 if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then |
|
75 let |
|
76 fun aux old_skolems |
|
77 (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) = |
|
78 let |
|
79 val (old_skolems, s) = |
|
80 if i = ~1 then |
|
81 (old_skolems, @{const_name undefined}) |
|
82 else case AList.find (op aconv) old_skolems t of |
|
83 s :: _ => (old_skolems, s) |
|
84 | [] => |
|
85 let |
|
86 val s = old_skolem_const_name i (length old_skolems) |
|
87 (length (Term.add_tvarsT T [])) |
|
88 in ((s, t) :: old_skolems, s) end |
|
89 in (old_skolems, Const (s, T)) end |
|
90 | aux old_skolems (t1 $ t2) = |
|
91 let |
|
92 val (old_skolems, t1) = aux old_skolems t1 |
|
93 val (old_skolems, t2) = aux old_skolems t2 |
|
94 in (old_skolems, t1 $ t2) end |
|
95 | aux old_skolems (Abs (s, T, t')) = |
|
96 let val (old_skolems, t') = aux old_skolems t' in |
|
97 (old_skolems, Abs (s, T, t')) |
|
98 end |
|
99 | aux old_skolems t = (old_skolems, t) |
|
100 in aux old_skolems t end |
|
101 else |
|
102 (old_skolems, t) |
|
103 |
|
104 fun reveal_old_skolem_terms old_skolems = |
|
105 map_aterms (fn t as Const (s, _) => |
|
106 if String.isPrefix old_skolem_const_prefix s then |
|
107 AList.lookup (op =) old_skolems s |> the |
|
108 |> map_types (map_type_tvar (K dummyT)) |
|
109 else |
|
110 t |
|
111 | t => t) |
|
112 |
|
113 fun reveal_lam_lifted lambdas = |
|
114 map_aterms (fn t as Const (s, _) => |
|
115 if String.isPrefix lam_lifted_prefix s then |
|
116 case AList.lookup (op =) lambdas s of |
|
117 SOME t => |
|
118 Const (@{const_name Metis.lambda}, dummyT) |
|
119 $ map_types (map_type_tvar (K dummyT)) |
|
120 (reveal_lam_lifted lambdas t) |
|
121 | NONE => t |
|
122 else |
|
123 t |
|
124 | t => t) |
|
125 |
|
126 |
|
127 (* ------------------------------------------------------------------------- *) |
|
128 (* Logic maps manage the interface between HOL and first-order logic. *) |
|
129 (* ------------------------------------------------------------------------- *) |
|
130 |
|
131 datatype isa_thm = |
|
132 Isa_Reflexive_or_Trivial | |
|
133 Isa_Lambda_Lifted | |
|
134 Isa_Raw of thm |
|
135 |
|
136 val proxy_defs = map (fst o snd o snd) proxy_table |
|
137 val prepare_helper = |
|
138 Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs) |
|
139 |
|
140 fun metis_term_from_atp type_enc (ATerm (s, tms)) = |
|
141 if is_tptp_variable s then |
|
142 Metis_Term.Var (Metis_Name.fromString s) |
|
143 else |
|
144 (case AList.lookup (op =) metis_name_table (s, length tms) of |
|
145 SOME (f, swap) => (f type_enc, swap) |
|
146 | NONE => (s, false)) |
|
147 |> (fn (s, swap) => |
|
148 Metis_Term.Fn (Metis_Name.fromString s, |
|
149 tms |> map (metis_term_from_atp type_enc) |
|
150 |> swap ? rev)) |
|
151 fun metis_atom_from_atp type_enc (AAtom tm) = |
|
152 (case metis_term_from_atp type_enc tm of |
|
153 Metis_Term.Fn x => x |
|
154 | _ => raise Fail "non CNF -- expected function") |
|
155 | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom" |
|
156 fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) = |
|
157 (false, metis_atom_from_atp type_enc phi) |
|
158 | metis_literal_from_atp type_enc phi = |
|
159 (true, metis_atom_from_atp type_enc phi) |
|
160 fun metis_literals_from_atp type_enc (AConn (AOr, phis)) = |
|
161 maps (metis_literals_from_atp type_enc) phis |
|
162 | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi] |
|
163 fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) = |
|
164 let |
|
165 fun some isa = |
|
166 SOME (phi |> metis_literals_from_atp type_enc |
|
167 |> Metis_LiteralSet.fromList |
|
168 |> Metis_Thm.axiom, isa) |
|
169 in |
|
170 if ident = type_tag_idempotence_helper_name orelse |
|
171 String.isPrefix tags_sym_formula_prefix ident then |
|
172 Isa_Reflexive_or_Trivial |> some |
|
173 else if String.isPrefix conjecture_prefix ident then |
|
174 NONE |
|
175 else if String.isPrefix helper_prefix ident then |
|
176 case (String.isSuffix typed_helper_suffix ident, |
|
177 space_explode "_" ident) of |
|
178 (needs_fairly_sound, _ :: const :: j :: _) => |
|
179 nth ((const, needs_fairly_sound) |
|
180 |> AList.lookup (op =) helper_table |> the) |
|
181 (the (Int.fromString j) - 1) |
|
182 |> prepare_helper |
|
183 |> Isa_Raw |> some |
|
184 | _ => raise Fail ("malformed helper identifier " ^ quote ident) |
|
185 else case try (unprefix fact_prefix) ident of |
|
186 SOME s => |
|
187 let val s = s |> space_explode "_" |> tl |> space_implode "_" |
|
188 in |
|
189 case Int.fromString s of |
|
190 SOME j => |
|
191 Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some |
|
192 | NONE => |
|
193 if String.isPrefix lam_fact_prefix (unascii_of s) then |
|
194 Isa_Lambda_Lifted |> some |
|
195 else |
|
196 raise Fail ("malformed fact identifier " ^ quote ident) |
|
197 end |
|
198 | NONE => TrueI |> Isa_Raw |> some |
|
199 end |
|
200 | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula" |
|
201 |
|
202 fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) = |
|
203 eliminate_lam_wrappers t |
|
204 | eliminate_lam_wrappers (t $ u) = |
|
205 eliminate_lam_wrappers t $ eliminate_lam_wrappers u |
|
206 | eliminate_lam_wrappers (Abs (s, T, t)) = |
|
207 Abs (s, T, eliminate_lam_wrappers t) |
|
208 | eliminate_lam_wrappers t = t |
|
209 |
|
210 (* Function to generate metis clauses, including comb and type clauses *) |
|
211 fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses = |
|
212 let |
|
213 val (conj_clauses, fact_clauses) = |
|
214 if polymorphism_of_type_enc type_enc = Polymorphic then |
|
215 (conj_clauses, fact_clauses) |
|
216 else |
|
217 conj_clauses @ fact_clauses |
|
218 |> map (pair 0) |
|
219 |> rpair (ctxt |> Config.put Monomorph.keep_partial_instances false) |
|
220 |-> Monomorph.monomorph atp_schematic_consts_of |
|
221 |> fst |> chop (length conj_clauses) |
|
222 |> pairself (maps (map (zero_var_indexes o snd))) |
|
223 val num_conjs = length conj_clauses |
|
224 val clauses = |
|
225 map2 (fn j => pair (Int.toString j, Local)) |
|
226 (0 upto num_conjs - 1) conj_clauses @ |
|
227 (* "General" below isn't quite correct; the fact could be local. *) |
|
228 map2 (fn j => pair (Int.toString (num_conjs + j), General)) |
|
229 (0 upto length fact_clauses - 1) fact_clauses |
|
230 val (old_skolems, props) = |
|
231 fold_rev (fn (name, th) => fn (old_skolems, props) => |
|
232 th |> prop_of |> Logic.strip_imp_concl |
|
233 |> conceal_old_skolem_terms (length clauses) old_skolems |
|
234 ||> lam_trans = lam_liftingN ? eliminate_lam_wrappers |
|
235 ||> (fn prop => (name, prop) :: props)) |
|
236 clauses ([], []) |
|
237 (* |
|
238 val _ = |
|
239 tracing ("PROPS:\n" ^ |
|
240 cat_lines (map (Syntax.string_of_term ctxt o snd) props)) |
|
241 *) |
|
242 val lam_trans = if lam_trans = combinatorsN then no_lamsN else lam_trans |
|
243 val (atp_problem, _, _, lifted, sym_tab) = |
|
244 prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans |
|
245 false false [] @{prop False} props |
|
246 (* |
|
247 val _ = tracing ("ATP PROBLEM: " ^ |
|
248 cat_lines (lines_for_atp_problem CNF atp_problem)) |
|
249 *) |
|
250 (* "rev" is for compatibility with existing proof scripts. *) |
|
251 val axioms = |
|
252 atp_problem |
|
253 |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev |
|
254 in (sym_tab, axioms, (lifted, old_skolems)) end |
|
255 |
|
256 end; |
|