ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
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
7 Translation of HOL to FOL for Metis.
10 signature METIS_TRANSLATE =
13 Isa_Reflexive_or_Trivial |
16 val metis_equal : string
17 val metis_predicator : string
18 val metis_app_op : string
19 val metis_type_tag : string
20 val metis_generated_var_prefix : string
21 val trace : bool Config.T
22 val verbose : bool Config.T
23 val trace_msg : Proof.context -> (unit -> string) -> unit
24 val verbose_warning : Proof.context -> string -> unit
25 val metis_name_table : ((string * int) * (string * bool)) list
26 val reveal_old_skolem_terms : (string * term) list -> term -> term
27 val prepare_metis_problem :
28 Proof.context -> string -> thm list -> thm list
29 -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list
32 structure Metis_Translate : METIS_TRANSLATE =
39 val metis_predicator = "{}"
40 val metis_app_op = "."
41 val metis_type_tag = ":"
42 val metis_generated_var_prefix = "_"
44 val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
45 val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
47 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
48 fun verbose_warning ctxt msg =
49 if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
51 val metis_name_table =
52 [((tptp_equal, 2), (metis_equal, false)),
53 ((tptp_old_equal, 2), (metis_equal, false)),
54 ((prefixed_predicator_name, 1), (metis_predicator, false)),
55 ((prefixed_app_op_name, 2), (metis_app_op, false)),
56 ((prefixed_type_tag_name, 2), (metis_type_tag, true))]
58 fun old_skolem_const_name i j num_T_args =
59 old_skolem_const_prefix ^ Long_Name.separator ^
60 (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))
62 fun conceal_old_skolem_terms i old_skolems t =
63 if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
66 (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) =
68 val (old_skolems, s) =
70 (old_skolems, @{const_name undefined})
71 else case AList.find (op aconv) old_skolems t of
72 s :: _ => (old_skolems, s)
75 val s = old_skolem_const_name i (length old_skolems)
76 (length (Term.add_tvarsT T []))
77 in ((s, t) :: old_skolems, s) end
78 in (old_skolems, Const (s, T)) end
79 | aux old_skolems (t1 $ t2) =
81 val (old_skolems, t1) = aux old_skolems t1
82 val (old_skolems, t2) = aux old_skolems t2
83 in (old_skolems, t1 $ t2) end
84 | aux old_skolems (Abs (s, T, t')) =
85 let val (old_skolems, t') = aux old_skolems t' in
86 (old_skolems, Abs (s, T, t'))
88 | aux old_skolems t = (old_skolems, t)
89 in aux old_skolems t end
93 fun reveal_old_skolem_terms old_skolems =
94 map_aterms (fn t as Const (s, _) =>
95 if String.isPrefix old_skolem_const_prefix s then
96 AList.lookup (op =) old_skolems s |> the
97 |> map_types (map_type_tvar (K dummyT))
103 (* ------------------------------------------------------------------------- *)
104 (* Logic maps manage the interface between HOL and first-order logic. *)
105 (* ------------------------------------------------------------------------- *)
108 Isa_Reflexive_or_Trivial |
111 val proxy_defs = map (fst o snd o snd) proxy_table
113 Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
115 fun metis_term_from_atp (ATerm (s, tms)) =
116 if is_tptp_variable s then
117 Metis_Term.Var (Metis_Name.fromString s)
120 val (s, swap) = AList.lookup (op =) metis_name_table (s, length tms)
121 |> the_default (s, false)
123 Metis_Term.Fn (Metis_Name.fromString s,
124 tms |> map metis_term_from_atp |> swap ? rev)
126 fun metis_atom_from_atp (AAtom tm) =
127 (case metis_term_from_atp tm of
129 | _ => raise Fail "non CNF -- expected function")
130 | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom"
131 fun metis_literal_from_atp (AConn (ANot, [phi])) =
132 (false, metis_atom_from_atp phi)
133 | metis_literal_from_atp phi = (true, metis_atom_from_atp phi)
134 fun metis_literals_from_atp (AConn (AOr, phis)) =
135 maps metis_literals_from_atp phis
136 | metis_literals_from_atp phi = [metis_literal_from_atp phi]
137 fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
140 SOME (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
141 |> Metis_Thm.axiom, isa)
143 if ident = type_tag_idempotence_helper_name orelse
144 String.isPrefix lightweight_tags_sym_formula_prefix ident then
145 Isa_Reflexive_or_Trivial |> some
146 else if String.isPrefix conjecture_prefix ident then
148 else if String.isPrefix helper_prefix ident then
149 case (String.isSuffix typed_helper_suffix ident,
150 space_explode "_" ident) of
151 (needs_fairly_sound, _ :: const :: j :: _) =>
152 nth ((const, needs_fairly_sound)
153 |> AList.lookup (op =) helper_table |> the)
154 (the (Int.fromString j) - 1)
157 | _ => raise Fail ("malformed helper identifier " ^ quote ident)
158 else case try (unprefix fact_prefix) ident of
161 val j = s |> space_explode "_" |> List.last |> Int.fromString |> the
162 in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
163 | NONE => TrueI |> Isa_Raw |> some
165 | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
167 (* Function to generate metis clauses, including comb and type clauses *)
168 fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
170 val type_enc = type_enc_from_string type_enc
171 val (conj_clauses, fact_clauses) =
172 if polymorphism_of_type_enc type_enc = Polymorphic then
173 (conj_clauses, fact_clauses)
175 conj_clauses @ fact_clauses
178 |-> Monomorph.monomorph atp_schematic_consts_of
179 |> fst |> chop (length conj_clauses)
180 |> pairself (maps (map (zero_var_indexes o snd)))
181 val num_conjs = length conj_clauses
183 map2 (fn j => pair (Int.toString j, Local))
184 (0 upto num_conjs - 1) conj_clauses @
185 (* "General" below isn't quite correct; the fact could be local. *)
186 map2 (fn j => pair (Int.toString (num_conjs + j), General))
187 (0 upto length fact_clauses - 1) fact_clauses
188 val (old_skolems, props) =
189 fold_rev (fn (name, th) => fn (old_skolems, props) =>
190 th |> prop_of |> Logic.strip_imp_concl
191 |> conceal_old_skolem_terms (length clauses) old_skolems
192 ||> (fn prop => (name, prop) :: props))
196 tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
198 val (atp_problem, _, _, _, _, _, sym_tab) =
199 prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
200 (rpair [] o map (introduce_combinators ctxt))
201 false false [] @{prop False} props
203 val _ = tracing ("ATP PROBLEM: " ^
204 cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
206 (* "rev" is for compatibility *)
208 atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
210 in (sym_tab, axioms, old_skolems) end