40 case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of |
40 case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of |
41 SOME ((s, _), (_, swap)) => (s, swap) |
41 SOME ((s, _), (_, swap)) => (s, swap) |
42 | _ => (s, false) |
42 | _ => (s, false) |
43 fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) = |
43 fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) = |
44 let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in |
44 let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in |
45 ATerm (s, tms |> map (atp_term_from_metis type_enc) |> swap ? rev) |
45 ATerm ((s, []), tms |> map (atp_term_from_metis type_enc) |> swap ? rev) |
46 end |
46 end |
47 | atp_term_from_metis _ (Metis_Term.Var s) = ATerm (Metis_Name.toString s, []) |
47 | atp_term_from_metis _ (Metis_Term.Var s) = |
|
48 ATerm ((Metis_Name.toString s, []), []) |
48 |
49 |
49 fun hol_term_from_metis ctxt type_enc sym_tab = |
50 fun hol_term_from_metis ctxt type_enc sym_tab = |
50 atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE |
51 atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE |
51 |
52 |
52 fun atp_literal_from_metis type_enc (pos, atom) = |
53 fun atp_literal_from_metis type_enc (pos, atom) = |
53 atom |> Metis_Term.Fn |> atp_term_from_metis type_enc |
54 atom |> Metis_Term.Fn |> atp_term_from_metis type_enc |
54 |> AAtom |> not pos ? mk_anot |
55 |> AAtom |> not pos ? mk_anot |
55 fun atp_clause_from_metis _ [] = AAtom (ATerm (tptp_false, [])) |
56 fun atp_clause_from_metis _ [] = AAtom (ATerm ((tptp_false, []), [])) |
56 | atp_clause_from_metis type_enc lits = |
57 | atp_clause_from_metis type_enc lits = |
57 lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr |
58 lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr |
58 |
59 |
59 fun polish_hol_terms ctxt (lifted, old_skolems) = |
60 fun polish_hol_terms ctxt (lifted, old_skolems) = |
60 map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems) |
61 map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems) |