1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML Mon Jan 23 17:40:32 2012 +0100
1.3 @@ -0,0 +1,256 @@
1.4 +(* Title: HOL/Tools/Metis/metis_generate.ML
1.5 + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
1.6 + Author: Kong W. Susanto, Cambridge University Computer Laboratory
1.7 + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
1.8 + Author: Jasmin Blanchette, TU Muenchen
1.9 +
1.10 +Translation of HOL to FOL for Metis.
1.11 +*)
1.12 +
1.13 +signature METIS_GENERATE =
1.14 +sig
1.15 + type type_enc = ATP_Problem_Generate.type_enc
1.16 +
1.17 + datatype isa_thm =
1.18 + Isa_Reflexive_or_Trivial |
1.19 + Isa_Lambda_Lifted |
1.20 + Isa_Raw of thm
1.21 +
1.22 + val metis_equal : string
1.23 + val metis_predicator : string
1.24 + val metis_app_op : string
1.25 + val metis_systematic_type_tag : string
1.26 + val metis_ad_hoc_type_tag : string
1.27 + val metis_generated_var_prefix : string
1.28 + val trace : bool Config.T
1.29 + val verbose : bool Config.T
1.30 + val trace_msg : Proof.context -> (unit -> string) -> unit
1.31 + val verbose_warning : Proof.context -> string -> unit
1.32 + val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
1.33 + val reveal_old_skolem_terms : (string * term) list -> term -> term
1.34 + val reveal_lam_lifted : (string * term) list -> term -> term
1.35 + val prepare_metis_problem :
1.36 + Proof.context -> type_enc -> string -> thm list -> thm list
1.37 + -> int Symtab.table * (Metis_Thm.thm * isa_thm) list
1.38 + * ((string * term) list * (string * term) list)
1.39 +end
1.40 +
1.41 +structure Metis_Generate : METIS_GENERATE =
1.42 +struct
1.43 +
1.44 +open ATP_Problem
1.45 +open ATP_Problem_Generate
1.46 +
1.47 +val metis_equal = "="
1.48 +val metis_predicator = "{}"
1.49 +val metis_app_op = Metis_Name.toString Metis_Term.appName
1.50 +val metis_systematic_type_tag =
1.51 + Metis_Name.toString Metis_Term.hasTypeFunctionName
1.52 +val metis_ad_hoc_type_tag = "**"
1.53 +val metis_generated_var_prefix = "_"
1.54 +
1.55 +val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
1.56 +val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
1.57 +
1.58 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
1.59 +fun verbose_warning ctxt msg =
1.60 + if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
1.61 +
1.62 +val metis_name_table =
1.63 + [((tptp_equal, 2), (K metis_equal, false)),
1.64 + ((tptp_old_equal, 2), (K metis_equal, false)),
1.65 + ((prefixed_predicator_name, 1), (K metis_predicator, false)),
1.66 + ((prefixed_app_op_name, 2), (K metis_app_op, false)),
1.67 + ((prefixed_type_tag_name, 2),
1.68 + (fn type_enc =>
1.69 + if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag
1.70 + else metis_ad_hoc_type_tag, true))]
1.71 +
1.72 +fun old_skolem_const_name i j num_T_args =
1.73 + old_skolem_const_prefix ^ Long_Name.separator ^
1.74 + (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))
1.75 +
1.76 +fun conceal_old_skolem_terms i old_skolems t =
1.77 + if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
1.78 + let
1.79 + fun aux old_skolems
1.80 + (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) =
1.81 + let
1.82 + val (old_skolems, s) =
1.83 + if i = ~1 then
1.84 + (old_skolems, @{const_name undefined})
1.85 + else case AList.find (op aconv) old_skolems t of
1.86 + s :: _ => (old_skolems, s)
1.87 + | [] =>
1.88 + let
1.89 + val s = old_skolem_const_name i (length old_skolems)
1.90 + (length (Term.add_tvarsT T []))
1.91 + in ((s, t) :: old_skolems, s) end
1.92 + in (old_skolems, Const (s, T)) end
1.93 + | aux old_skolems (t1 $ t2) =
1.94 + let
1.95 + val (old_skolems, t1) = aux old_skolems t1
1.96 + val (old_skolems, t2) = aux old_skolems t2
1.97 + in (old_skolems, t1 $ t2) end
1.98 + | aux old_skolems (Abs (s, T, t')) =
1.99 + let val (old_skolems, t') = aux old_skolems t' in
1.100 + (old_skolems, Abs (s, T, t'))
1.101 + end
1.102 + | aux old_skolems t = (old_skolems, t)
1.103 + in aux old_skolems t end
1.104 + else
1.105 + (old_skolems, t)
1.106 +
1.107 +fun reveal_old_skolem_terms old_skolems =
1.108 + map_aterms (fn t as Const (s, _) =>
1.109 + if String.isPrefix old_skolem_const_prefix s then
1.110 + AList.lookup (op =) old_skolems s |> the
1.111 + |> map_types (map_type_tvar (K dummyT))
1.112 + else
1.113 + t
1.114 + | t => t)
1.115 +
1.116 +fun reveal_lam_lifted lambdas =
1.117 + map_aterms (fn t as Const (s, _) =>
1.118 + if String.isPrefix lam_lifted_prefix s then
1.119 + case AList.lookup (op =) lambdas s of
1.120 + SOME t =>
1.121 + Const (@{const_name Metis.lambda}, dummyT)
1.122 + $ map_types (map_type_tvar (K dummyT))
1.123 + (reveal_lam_lifted lambdas t)
1.124 + | NONE => t
1.125 + else
1.126 + t
1.127 + | t => t)
1.128 +
1.129 +
1.130 +(* ------------------------------------------------------------------------- *)
1.131 +(* Logic maps manage the interface between HOL and first-order logic. *)
1.132 +(* ------------------------------------------------------------------------- *)
1.133 +
1.134 +datatype isa_thm =
1.135 + Isa_Reflexive_or_Trivial |
1.136 + Isa_Lambda_Lifted |
1.137 + Isa_Raw of thm
1.138 +
1.139 +val proxy_defs = map (fst o snd o snd) proxy_table
1.140 +val prepare_helper =
1.141 + Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
1.142 +
1.143 +fun metis_term_from_atp type_enc (ATerm (s, tms)) =
1.144 + if is_tptp_variable s then
1.145 + Metis_Term.Var (Metis_Name.fromString s)
1.146 + else
1.147 + (case AList.lookup (op =) metis_name_table (s, length tms) of
1.148 + SOME (f, swap) => (f type_enc, swap)
1.149 + | NONE => (s, false))
1.150 + |> (fn (s, swap) =>
1.151 + Metis_Term.Fn (Metis_Name.fromString s,
1.152 + tms |> map (metis_term_from_atp type_enc)
1.153 + |> swap ? rev))
1.154 +fun metis_atom_from_atp type_enc (AAtom tm) =
1.155 + (case metis_term_from_atp type_enc tm of
1.156 + Metis_Term.Fn x => x
1.157 + | _ => raise Fail "non CNF -- expected function")
1.158 + | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom"
1.159 +fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) =
1.160 + (false, metis_atom_from_atp type_enc phi)
1.161 + | metis_literal_from_atp type_enc phi =
1.162 + (true, metis_atom_from_atp type_enc phi)
1.163 +fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
1.164 + maps (metis_literals_from_atp type_enc) phis
1.165 + | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
1.166 +fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) =
1.167 + let
1.168 + fun some isa =
1.169 + SOME (phi |> metis_literals_from_atp type_enc
1.170 + |> Metis_LiteralSet.fromList
1.171 + |> Metis_Thm.axiom, isa)
1.172 + in
1.173 + if ident = type_tag_idempotence_helper_name orelse
1.174 + String.isPrefix tags_sym_formula_prefix ident then
1.175 + Isa_Reflexive_or_Trivial |> some
1.176 + else if String.isPrefix conjecture_prefix ident then
1.177 + NONE
1.178 + else if String.isPrefix helper_prefix ident then
1.179 + case (String.isSuffix typed_helper_suffix ident,
1.180 + space_explode "_" ident) of
1.181 + (needs_fairly_sound, _ :: const :: j :: _) =>
1.182 + nth ((const, needs_fairly_sound)
1.183 + |> AList.lookup (op =) helper_table |> the)
1.184 + (the (Int.fromString j) - 1)
1.185 + |> prepare_helper
1.186 + |> Isa_Raw |> some
1.187 + | _ => raise Fail ("malformed helper identifier " ^ quote ident)
1.188 + else case try (unprefix fact_prefix) ident of
1.189 + SOME s =>
1.190 + let val s = s |> space_explode "_" |> tl |> space_implode "_"
1.191 + in
1.192 + case Int.fromString s of
1.193 + SOME j =>
1.194 + Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
1.195 + | NONE =>
1.196 + if String.isPrefix lam_fact_prefix (unascii_of s) then
1.197 + Isa_Lambda_Lifted |> some
1.198 + else
1.199 + raise Fail ("malformed fact identifier " ^ quote ident)
1.200 + end
1.201 + | NONE => TrueI |> Isa_Raw |> some
1.202 + end
1.203 + | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
1.204 +
1.205 +fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
1.206 + eliminate_lam_wrappers t
1.207 + | eliminate_lam_wrappers (t $ u) =
1.208 + eliminate_lam_wrappers t $ eliminate_lam_wrappers u
1.209 + | eliminate_lam_wrappers (Abs (s, T, t)) =
1.210 + Abs (s, T, eliminate_lam_wrappers t)
1.211 + | eliminate_lam_wrappers t = t
1.212 +
1.213 +(* Function to generate metis clauses, including comb and type clauses *)
1.214 +fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
1.215 + let
1.216 + val (conj_clauses, fact_clauses) =
1.217 + if polymorphism_of_type_enc type_enc = Polymorphic then
1.218 + (conj_clauses, fact_clauses)
1.219 + else
1.220 + conj_clauses @ fact_clauses
1.221 + |> map (pair 0)
1.222 + |> rpair (ctxt |> Config.put Monomorph.keep_partial_instances false)
1.223 + |-> Monomorph.monomorph atp_schematic_consts_of
1.224 + |> fst |> chop (length conj_clauses)
1.225 + |> pairself (maps (map (zero_var_indexes o snd)))
1.226 + val num_conjs = length conj_clauses
1.227 + val clauses =
1.228 + map2 (fn j => pair (Int.toString j, Local))
1.229 + (0 upto num_conjs - 1) conj_clauses @
1.230 + (* "General" below isn't quite correct; the fact could be local. *)
1.231 + map2 (fn j => pair (Int.toString (num_conjs + j), General))
1.232 + (0 upto length fact_clauses - 1) fact_clauses
1.233 + val (old_skolems, props) =
1.234 + fold_rev (fn (name, th) => fn (old_skolems, props) =>
1.235 + th |> prop_of |> Logic.strip_imp_concl
1.236 + |> conceal_old_skolem_terms (length clauses) old_skolems
1.237 + ||> lam_trans = lam_liftingN ? eliminate_lam_wrappers
1.238 + ||> (fn prop => (name, prop) :: props))
1.239 + clauses ([], [])
1.240 + (*
1.241 + val _ =
1.242 + tracing ("PROPS:\n" ^
1.243 + cat_lines (map (Syntax.string_of_term ctxt o snd) props))
1.244 + *)
1.245 + val lam_trans = if lam_trans = combinatorsN then no_lamsN else lam_trans
1.246 + val (atp_problem, _, _, lifted, sym_tab) =
1.247 + prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
1.248 + false false [] @{prop False} props
1.249 + (*
1.250 + val _ = tracing ("ATP PROBLEM: " ^
1.251 + cat_lines (lines_for_atp_problem CNF atp_problem))
1.252 + *)
1.253 + (* "rev" is for compatibility with existing proof scripts. *)
1.254 + val axioms =
1.255 + atp_problem
1.256 + |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
1.257 + in (sym_tab, axioms, (lifted, old_skolems)) end
1.258 +
1.259 +end;