src/HOL/Tools/Metis/metis_translate.ML

more work on new metis that exploits the powerful new type encodings

(*  Title:      HOL/Tools/Metis/metis_translate.ML
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
    Author:     Jasmin Blanchette, TU Muenchen

Translation of HOL to FOL for Metis.
*)

signature METIS_TRANSLATE =
sig
  type type_literal = ATP_Translate.type_literal

  datatype mode = FO | HO | FT | New

  type metis_problem =
    {axioms: (Metis_Thm.thm * thm) list,
     tfrees: type_literal list,
     old_skolems: (string * term) list}

  val metis_generated_var_prefix : string
  val new_skolem_const_prefix : string
  val num_type_args: theory -> string -> int
  val new_skolem_var_name_from_const : string -> string
  val reveal_old_skolem_terms : (string * term) list -> term -> term
  val string_of_mode : mode -> string
  val prepare_metis_problem :
    Proof.context -> mode -> thm list -> thm list -> mode * metis_problem
end

structure Metis_Translate : METIS_TRANSLATE =
struct

open ATP_Problem
open ATP_Translate

val metis_generated_var_prefix = "_"

(* The number of type arguments of a constant, zero if it's monomorphic. For
   (instances of) Skolem pseudoconstants, this information is encoded in the
   constant name. *)
fun num_type_args thy s =
  if String.isPrefix skolem_const_prefix s then
    s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
  else
    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length

fun new_skolem_var_name_from_const s =
  let val ss = s |> space_explode Long_Name.separator in
    nth ss (length ss - 2)
  end

fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
  | predicate_of thy (t, pos) =
    (combterm_from_term thy [] (Envir.eta_contract t), pos)

fun literals_of_term1 args thy (@{const Trueprop} $ P) =
    literals_of_term1 args thy P
  | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
    literals_of_term1 (literals_of_term1 args thy P) thy Q
  | literals_of_term1 (lits, ts) thy P =
    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
      ((pol, pred) :: lits, union (op =) ts ts')
    end
val literals_of_term = literals_of_term1 ([], [])

fun old_skolem_const_name i j num_T_args =
  old_skolem_const_prefix ^ Long_Name.separator ^
  (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))

fun conceal_old_skolem_terms i old_skolems t =
  if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
    let
      fun aux old_skolems
             (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) =
          let
            val (old_skolems, s) =
              if i = ~1 then
                (old_skolems, @{const_name undefined})
              else case AList.find (op aconv) old_skolems t of
                s :: _ => (old_skolems, s)
              | [] =>
                let
                  val s = old_skolem_const_name i (length old_skolems)
                                                (length (Term.add_tvarsT T []))
                in ((s, t) :: old_skolems, s) end
          in (old_skolems, Const (s, T)) end
        | aux old_skolems (t1 $ t2) =
          let
            val (old_skolems, t1) = aux old_skolems t1
            val (old_skolems, t2) = aux old_skolems t2
          in (old_skolems, t1 $ t2) end
        | aux old_skolems (Abs (s, T, t')) =
          let val (old_skolems, t') = aux old_skolems t' in
            (old_skolems, Abs (s, T, t'))
          end
        | aux old_skolems t = (old_skolems, t)
    in aux old_skolems t end
  else
    (old_skolems, t)

fun reveal_old_skolem_terms old_skolems =
  map_aterms (fn t as Const (s, _) =>
                 if String.isPrefix old_skolem_const_prefix s then
                   AList.lookup (op =) old_skolems s |> the
                   |> map_types Type_Infer.paramify_vars
                 else
                   t
               | t => t)


(* ------------------------------------------------------------------------- *)
(* HOL to FOL  (Isabelle to Metis)                                           *)
(* ------------------------------------------------------------------------- *)

(* first-order, higher-order, fully-typed, new *)
datatype mode = FO | HO | FT | New

fun string_of_mode FO = "FO"
  | string_of_mode HO = "HO"
  | string_of_mode FT = "FT"
  | string_of_mode New = "New"

fun fn_isa_to_met_sublevel "equal" = "c_fequal"
  | fn_isa_to_met_sublevel "c_False" = "c_fFalse"
  | fn_isa_to_met_sublevel "c_True" = "c_fTrue"
  | fn_isa_to_met_sublevel "c_Not" = "c_fNot"
  | fn_isa_to_met_sublevel "c_conj" = "c_fconj"
  | fn_isa_to_met_sublevel "c_disj" = "c_fdisj"
  | fn_isa_to_met_sublevel "c_implies" = "c_fimplies"
  | fn_isa_to_met_sublevel x = x

fun fn_isa_to_met_toplevel "equal" = "="
  | fn_isa_to_met_toplevel x = x

fun metis_lit b c args = (b, (c, args));

fun metis_term_from_typ (Type (s, Ts)) =
    Metis_Term.Fn (make_fixed_type_const s, map metis_term_from_typ Ts)
  | metis_term_from_typ (TFree (s, _)) =
    Metis_Term.Fn (make_fixed_type_var s, [])
  | metis_term_from_typ (TVar (x, _)) =
    Metis_Term.Var (make_schematic_type_var x)

(*These two functions insert type literals before the real literals. That is the
  opposite order from TPTP linkup, but maybe OK.*)

fun hol_term_to_fol_FO tm =
  case strip_combterm_comb tm of
      (CombConst ((c, _), _, Ts), tms) =>
        let val tyargs = map metis_term_from_typ Ts
            val args = map hol_term_to_fol_FO tms
        in Metis_Term.Fn (c, tyargs @ args) end
    | (CombVar ((v, _), _), []) => Metis_Term.Var v
    | _ => raise Fail "non-first-order combterm"

fun hol_term_to_fol_HO (CombConst ((a, _), _, Ts)) =
      Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_typ Ts)
  | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
  | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
       Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);

(*The fully-typed translation, to avoid type errors*)
fun tag_with_type tm T =
  Metis_Term.Fn (type_tag_name, [tm, metis_term_from_typ T])

fun hol_term_to_fol_FT (CombVar ((s, _), ty)) =
    tag_with_type (Metis_Term.Var s) ty
  | hol_term_to_fol_FT (CombConst ((a, _), ty, _)) =
    tag_with_type (Metis_Term.Fn (fn_isa_to_met_sublevel a, [])) ty
  | hol_term_to_fol_FT (tm as CombApp (tm1,tm2)) =
    tag_with_type (Metis_Term.Fn (".", map hol_term_to_fol_FT [tm1, tm2]))
                  (combtyp_of tm)

fun hol_literal_to_fol FO (pos, tm) =
      let
        val (CombConst((p, _), _, Ts), tms) = strip_combterm_comb tm
        val tylits = if p = "equal" then [] else map metis_term_from_typ Ts
        val lits = map hol_term_to_fol_FO tms
      in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
  | hol_literal_to_fol HO (pos, tm) =
     (case strip_combterm_comb tm of
          (CombConst(("equal", _), _, _), tms) =>
            metis_lit pos "=" (map hol_term_to_fol_HO tms)
        | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
  | hol_literal_to_fol FT (pos, tm) =
     (case strip_combterm_comb tm of
          (CombConst(("equal", _), _, _), tms) =>
            metis_lit pos "=" (map hol_term_to_fol_FT tms)
        | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);

fun literals_of_hol_term thy mode t =
  let val (lits, types_sorts) = literals_of_term thy t in
    (map (hol_literal_to_fol mode) lits, types_sorts)
  end

(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
    metis_lit pos s [Metis_Term.Var s']
  | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
    metis_lit pos s [Metis_Term.Fn (s',[])]

fun has_default_sort _ (TVar _) = false
  | has_default_sort ctxt (TFree (x, s)) =
    (s = the_default [] (Variable.def_sort ctxt (x, ~1)));

fun metis_of_tfree tf =
  Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));

fun hol_thm_to_fol is_conjecture ctxt mode j old_skolems th =
  let
    val thy = Proof_Context.theory_of ctxt
    val (old_skolems, (mlits, types_sorts)) =
     th |> prop_of |> Logic.strip_imp_concl
        |> conceal_old_skolem_terms j old_skolems
        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
  in
    if is_conjecture then
      (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
       raw_type_literals_for_types types_sorts, old_skolems)
    else
      let
        val tylits = types_sorts |> filter_out (has_default_sort ctxt)
                                 |> raw_type_literals_for_types
        val mtylits = map (metis_of_type_literals false) tylits
      in
        (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
         old_skolems)
      end
  end;

(* ------------------------------------------------------------------------- *)
(* Logic maps manage the interface between HOL and first-order logic.        *)
(* ------------------------------------------------------------------------- *)

type metis_problem =
  {axioms: (Metis_Thm.thm * thm) list,
   tfrees: type_literal list,
   old_skolems: (string * term) list}

fun is_quasi_fol_clause thy =
  Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of

(*Extract TFree constraints from context to include as conjecture clauses*)
fun init_tfrees ctxt =
  let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
    Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
    |> raw_type_literals_for_types
  end;

fun const_in_metis c (pred, tm_list) =
  let
    fun in_mterm (Metis_Term.Var _) = false
      | in_mterm (Metis_Term.Fn (nm, tm_list)) =
        c = nm orelse exists in_mterm tm_list
  in c = pred orelse exists in_mterm tm_list end

(* ARITY CLAUSE *)
fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
    metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
  | m_arity_cls (TVarLit ((c, _), (s, _))) =
    metis_lit false c [Metis_Term.Var s]
(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
fun arity_cls ({prem_lits, concl_lits, ...} : arity_clause) =
  (TrueI,
   Metis_Thm.axiom (Metis_LiteralSet.fromList
                        (map m_arity_cls (concl_lits :: prem_lits))));

(* CLASSREL CLAUSE *)
fun m_class_rel_cls (subclass, _) (superclass, _) =
  [metis_lit false subclass [Metis_Term.Var "T"],
   metis_lit true superclass [Metis_Term.Var "T"]]
fun class_rel_cls ({subclass, superclass, ...} : class_rel_clause) =
  (TrueI, m_class_rel_cls subclass superclass
          |> Metis_LiteralSet.fromList |> Metis_Thm.axiom)

fun type_ext thy tms =
  let
    val subs = tfree_classes_of_terms tms
    val supers = tvar_classes_of_terms tms
    val tycons = type_consts_of_terms thy tms
    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
    val class_rel_clauses = make_class_rel_clauses thy subs supers'
  in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end

fun metis_name_from_atp s =
  if is_tptp_equal s then "="
  else if s = predicator_name then "{}"
  else if s = app_op_name then "."
  else s
fun metis_term_from_atp (ATerm (s, tms)) =
  if is_tptp_variable s then Metis_Term.Var s
  else Metis_Term.Fn (metis_name_from_atp s, map metis_term_from_atp tms)
fun metis_atom_from_atp (AAtom (ATerm (s, tms))) =
    (metis_name_from_atp s, map metis_term_from_atp tms)
  | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom"
fun metis_literal_from_atp (AConn (ANot, [phi])) =
    (false, metis_atom_from_atp phi)
  | metis_literal_from_atp phi = (true, metis_atom_from_atp phi)
fun metis_literals_from_atp (AConn (AOr, [phi1, phi2])) =
    uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2))
  | metis_literals_from_atp phi = [metis_literal_from_atp phi]
fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
    let val j = ident |> unprefix conjecture_prefix |> Int.fromString |> the in
      (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
           |> Metis_Thm.axiom,
       Meson.make_meta_clause (nth clauses j))
    end
  | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"

(* Function to generate metis clauses, including comb and type clauses *)
fun prepare_metis_problem ctxt New conj_clauses fact_clauses =
    let
      val type_sys = Preds (Polymorphic, (* Nonmonotonic_Types FIXME ### *) No_Types, Light)
      val explicit_apply = NONE
      val clauses = conj_clauses @ fact_clauses
      val (atp_problem, pool, _, _, _, _, sym_tab) =
        prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys
                            explicit_apply false (map prop_of clauses)
                            @{prop False} []
      (* val _ = tracing (PolyML.makestring atp_problem) FIXME ### *)
      val axioms =
        atp_problem
        |> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd)
    in (New, {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)}) end
  | prepare_metis_problem ctxt mode conj_clauses fact_clauses =
    let
      val thy = Proof_Context.theory_of ctxt
      (* The modes FO and FT are sticky. HO can be downgraded to FO. *)
      val mode =
        if mode = HO andalso
           forall (forall (is_quasi_fol_clause thy))
                  [conj_clauses, fact_clauses] then
          FO
        else
          mode
      fun add_thm is_conjecture (isa_ith, metis_ith)
                  {axioms, tfrees, old_skolems} : metis_problem =
        let
          val (mth, tfree_lits, old_skolems) =
            hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems
                           metis_ith
        in
          {axioms = (mth, isa_ith) :: axioms,
           tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
        end;
      fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} =
        {axioms = (mth, ith) :: axioms, tfrees = tfrees,
         old_skolems = old_skolems}
      fun add_tfrees {axioms, tfrees, old_skolems} =
        {axioms =
           map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ axioms,
         tfrees = tfrees, old_skolems = old_skolems}
      val problem =
        {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
        |> fold (add_thm true o `Meson.make_meta_clause) conj_clauses
        |> add_tfrees
        |> fold (add_thm false o `Meson.make_meta_clause) fact_clauses
      val clause_lists = map (Metis_Thm.clause o #1) (#axioms problem)
      fun is_used c =
        exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
      val problem =
        if mode = FO then
          problem
        else
          let
            val fdefs = @{thms fFalse_def fTrue_def fNot_def fconj_def fdisj_def
                               fimplies_def fequal_def}
            val prepare_helper =
              zero_var_indexes
              #> `(Meson.make_meta_clause
                   #> rewrite_rule (map safe_mk_meta_eq fdefs))
            val helper_ths =
              helper_table
              |> filter (is_used o prefix const_prefix o fst)
              |> maps (fn (_, (needs_full_types, thms)) =>
                          if needs_full_types andalso mode <> FT then []
                          else map prepare_helper thms)
          in problem |> fold (add_thm false) helper_ths end
      val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses))
    in (mode, fold add_type_thm type_ths problem) end

end;