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