(*  Title:      HOL/Tools/ATP/atp_translate.ML

    Author:     Fabian Immler, TU Muenchen

    Author:     Makarius

    Author:     Jasmin Blanchette, TU Muenchen

Translation of HOL to FOL for Sledgehammer.

*)

signature ATP_TRANSLATE =

sig

  type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term

  type connective = ATP_Problem.connective

  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula

  type format = ATP_Problem.format

  type formula_kind = ATP_Problem.formula_kind

  type 'a problem = 'a ATP_Problem.problem

  datatype locality =

    General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |

    Chained

  datatype order = First_Order | Higher_Order

  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic

  datatype type_level =

    All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |

    No_Types

  datatype type_heaviness = Heavyweight | Lightweight

  datatype type_enc =

    Simple_Types of order * type_level |

    Preds of polymorphism * type_level * type_heaviness |

    Tags of polymorphism * type_level * type_heaviness

  val bound_var_prefix : string

  val schematic_var_prefix : string

  val fixed_var_prefix : string

  val tvar_prefix : string

  val tfree_prefix : string

  val const_prefix : string

  val type_const_prefix : string

  val class_prefix : string

  val skolem_const_prefix : string

  val old_skolem_const_prefix : string

  val new_skolem_const_prefix : string

  val type_decl_prefix : string

  val sym_decl_prefix : string

  val preds_sym_formula_prefix : string

  val lightweight_tags_sym_formula_prefix : string

  val fact_prefix : string

  val conjecture_prefix : string

  val helper_prefix : string

  val class_rel_clause_prefix : string

  val arity_clause_prefix : string

  val tfree_clause_prefix : string

  val typed_helper_suffix : string

  val untyped_helper_suffix : string

  val type_tag_idempotence_helper_name : string

  val predicator_name : string

  val app_op_name : string

  val type_tag_name : string

  val type_pred_name : string

  val simple_type_prefix : string

  val prefixed_predicator_name : string

  val prefixed_app_op_name : string

  val prefixed_type_tag_name : string

  val ascii_of : string -> string

  val unascii_of : string -> string

  val strip_prefix_and_unascii : string -> string -> string option

  val proxy_table : (string * (string * (thm * (string * string)))) list

  val proxify_const : string -> (string * string) option

  val invert_const : string -> string

  val unproxify_const : string -> string

  val new_skolem_var_name_from_const : string -> string

  val num_type_args : theory -> string -> int

  val atp_irrelevant_consts : string list

  val atp_schematic_consts_of : term -> typ list Symtab.table

  val is_locality_global : locality -> bool

  val type_enc_from_string : string -> type_enc

  val polymorphism_of_type_enc : type_enc -> polymorphism

  val level_of_type_enc : type_enc -> type_level

  val is_type_enc_virtually_sound : type_enc -> bool

  val is_type_enc_fairly_sound : type_enc -> bool

  val choose_format : format list -> type_enc -> format * type_enc

  val mk_aconns :

    connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula

  val unmangled_const : string -> string * (string, 'b) ho_term list

  val unmangled_const_name : string -> string

  val helper_table : ((string * bool) * thm list) list

  val factsN : string

  val prepare_atp_problem :

    Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool

    -> bool -> bool -> bool -> term list -> term

    -> ((string * locality) * term) list

    -> string problem * string Symtab.table * int * int

       * (string * locality) list vector * int list * int Symtab.table

  val atp_problem_weights : string problem -> (string * real) list

end;

structure ATP_Translate : ATP_TRANSLATE =

struct

open ATP_Util

open ATP_Problem

type name = string * string

(* experimental *)

val generate_useful_info = false

fun useful_isabelle_info s =

  if generate_useful_info then

    SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))

  else

    NONE

val intro_info = useful_isabelle_info "intro"

val elim_info = useful_isabelle_info "elim"

val simp_info = useful_isabelle_info "simp"

val bound_var_prefix = "B_"

val schematic_var_prefix = "V_"

val fixed_var_prefix = "v_"

val tvar_prefix = "T_"

val tfree_prefix = "t_"

val const_prefix = "c_"

val type_const_prefix = "tc_"

val class_prefix = "cl_"

val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"

val old_skolem_const_prefix = skolem_const_prefix ^ "o"

val new_skolem_const_prefix = skolem_const_prefix ^ "n"

val type_decl_prefix = "ty_"

val sym_decl_prefix = "sy_"

val preds_sym_formula_prefix = "psy_"

val lightweight_tags_sym_formula_prefix = "tsy_"

val fact_prefix = "fact_"

val conjecture_prefix = "conj_"

val helper_prefix = "help_"

val class_rel_clause_prefix = "clar_"

val arity_clause_prefix = "arity_"

val tfree_clause_prefix = "tfree_"

val typed_helper_suffix = "_T"

val untyped_helper_suffix = "_U"

val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"

val predicator_name = "hBOOL"

val app_op_name = "hAPP"

val type_tag_name = "ti"

val type_pred_name = "is"

val simple_type_prefix = "ty_"

val prefixed_predicator_name = const_prefix ^ predicator_name

val prefixed_app_op_name = const_prefix ^ app_op_name

val prefixed_type_tag_name = const_prefix ^ type_tag_name

(* Freshness almost guaranteed! *)

val sledgehammer_weak_prefix = "Sledgehammer:"

(*Escaping of special characters.

  Alphanumeric characters are left unchanged.

  The character _ goes to __

  Characters in the range ASCII space to / go to _A to _P, respectively.

  Other characters go to _nnn where nnn is the decimal ASCII code.*)

val upper_a_minus_space = Char.ord #"A" - Char.ord #" "

fun stringN_of_int 0 _ = ""

  | stringN_of_int k n =

    stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)

fun ascii_of_char c =

  if Char.isAlphaNum c then

    String.str c

  else if c = #"_" then

    "__"

  else if #" " <= c andalso c <= #"/" then

    "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))

  else

    (* fixed width, in case more digits follow *)

    "_" ^ stringN_of_int 3 (Char.ord c)

val ascii_of = String.translate ascii_of_char

(** Remove ASCII armoring from names in proof files **)

(* We don't raise error exceptions because this code can run inside a worker

   thread. Also, the errors are impossible. *)

val unascii_of =

  let

    fun un rcs [] = String.implode(rev rcs)

      | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)

        (* Three types of _ escapes: __, _A to _P, _nnn *)

      | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs

      | un rcs (#"_" :: c :: cs) =

        if #"A" <= c andalso c<= #"P" then

          (* translation of #" " to #"/" *)

          un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs

        else

          let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in

            case Int.fromString (String.implode digits) of

              SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))

            | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)

          end

      | un rcs (c :: cs) = un (c :: rcs) cs

  in un [] o String.explode end

(* If string s has the prefix s1, return the result of deleting it,

   un-ASCII'd. *)

fun strip_prefix_and_unascii s1 s =

  if String.isPrefix s1 s then

    SOME (unascii_of (String.extract (s, size s1, NONE)))

  else

    NONE

val proxy_table =

  [("c_False", (@{const_name False}, (@{thm fFalse_def},

       ("fFalse", @{const_name ATP.fFalse})))),

   ("c_True", (@{const_name True}, (@{thm fTrue_def},

       ("fTrue", @{const_name ATP.fTrue})))),

   ("c_Not", (@{const_name Not}, (@{thm fNot_def},

       ("fNot", @{const_name ATP.fNot})))),

   ("c_conj", (@{const_name conj}, (@{thm fconj_def},

       ("fconj", @{const_name ATP.fconj})))),

   ("c_disj", (@{const_name disj}, (@{thm fdisj_def},

       ("fdisj", @{const_name ATP.fdisj})))),

   ("c_implies", (@{const_name implies}, (@{thm fimplies_def},

       ("fimplies", @{const_name ATP.fimplies})))),

   ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},

       ("fequal", @{const_name ATP.fequal})))),

   ("c_All", (@{const_name All}, (@{thm fAll_def},

       ("fAll", @{const_name ATP.fAll})))),

   ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},

       ("fEx", @{const_name ATP.fEx}))))]

val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)

(* Readable names for the more common symbolic functions. Do not mess with the

   table unless you know what you are doing. *)

val const_trans_table =

  [(@{type_name Product_Type.prod}, "prod"),

   (@{type_name Sum_Type.sum}, "sum"),

   (@{const_name False}, "False"),

   (@{const_name True}, "True"),

   (@{const_name Not}, "Not"),

   (@{const_name conj}, "conj"),

   (@{const_name disj}, "disj"),

   (@{const_name implies}, "implies"),

   (@{const_name HOL.eq}, "equal"),

   (@{const_name All}, "All"),

   (@{const_name Ex}, "Ex"),

   (@{const_name If}, "If"),

   (@{const_name Set.member}, "member"),

   (@{const_name Meson.COMBI}, "COMBI"),

   (@{const_name Meson.COMBK}, "COMBK"),

   (@{const_name Meson.COMBB}, "COMBB"),

   (@{const_name Meson.COMBC}, "COMBC"),

   (@{const_name Meson.COMBS}, "COMBS")]

  |> Symtab.make

  |> fold (Symtab.update o swap o snd o snd o snd) proxy_table

(* Invert the table of translations between Isabelle and ATPs. *)

val const_trans_table_inv =

  const_trans_table |> Symtab.dest |> map swap |> Symtab.make

val const_trans_table_unprox =

  Symtab.empty

  |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table

val invert_const = perhaps (Symtab.lookup const_trans_table_inv)

val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)

fun lookup_const c =

  case Symtab.lookup const_trans_table c of

    SOME c' => c'

  | NONE => ascii_of c

fun ascii_of_indexname (v, 0) = ascii_of v

  | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i

fun make_bound_var x = bound_var_prefix ^ ascii_of x

fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v

fun make_fixed_var x = fixed_var_prefix ^ ascii_of x

fun make_schematic_type_var (x, i) =

      tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))

fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))

(* "HOL.eq" is mapped to the ATP's equality. *)

fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal

  | make_fixed_const c = const_prefix ^ lookup_const c

fun make_fixed_type_const c = type_const_prefix ^ lookup_const c

fun make_type_class clas = class_prefix ^ ascii_of clas

fun new_skolem_var_name_from_const s =

  let val ss = s |> space_explode Long_Name.separator in

    nth ss (length ss - 2)

  end

(* 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

(* These are either simplified away by "Meson.presimplify" (most of the time) or

   handled specially via "fFalse", "fTrue", ..., "fequal". *)

val atp_irrelevant_consts =

  [@{const_name False}, @{const_name True}, @{const_name Not},

   @{const_name conj}, @{const_name disj}, @{const_name implies},

   @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]

val atp_monomorph_bad_consts =

  atp_irrelevant_consts @

  (* These are ignored anyway by the relevance filter (unless they appear in

     higher-order places) but not by the monomorphizer. *)

  [@{const_name all}, @{const_name "==>"}, @{const_name "=="},

   @{const_name Trueprop}, @{const_name All}, @{const_name Ex},

   @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]

fun add_schematic_const (x as (_, T)) =

  Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x

val add_schematic_consts_of =

  Term.fold_aterms (fn Const (x as (s, _)) =>

                       not (member (op =) atp_monomorph_bad_consts s)

                       ? add_schematic_const x

                      | _ => I)

fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty

(** Definitions and functions for FOL clauses and formulas for TPTP **)

(* The first component is the type class; the second is a "TVar" or "TFree". *)

datatype type_literal =

  TyLitVar of name * name |

  TyLitFree of name * name

(** Isabelle arities **)

datatype arity_literal =

  TConsLit of name * name * name list |

  TVarLit of name * name

fun gen_TVars 0 = []

  | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)

val type_class = the_single @{sort type}

fun add_packed_sort tvar =

  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))

type arity_clause =

  {name : string,

   prem_lits : arity_literal list,

   concl_lits : arity_literal}

(* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)

fun make_axiom_arity_clause (tcons, name, (cls, args)) =

  let

    val tvars = gen_TVars (length args)

    val tvars_srts = ListPair.zip (tvars, args)

  in

    {name = name,

     prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,

     concl_lits = TConsLit (`make_type_class cls,

                            `make_fixed_type_const tcons,

                            tvars ~~ tvars)}

  end

fun arity_clause _ _ (_, []) = []

  | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =  (* ignore *)

    arity_clause seen n (tcons, ars)

  | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =

    if member (op =) seen class then

      (* multiple arities for the same (tycon, class) pair *)

      make_axiom_arity_clause (tcons,

          lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,

          ar) ::

      arity_clause seen (n + 1) (tcons, ars)

    else

      make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^

                               ascii_of class, ar) ::

      arity_clause (class :: seen) n (tcons, ars)

fun multi_arity_clause [] = []

  | multi_arity_clause ((tcons, ars) :: tc_arlists) =

      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists

(* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in

   theory thy provided its arguments have the corresponding sorts. *)

fun type_class_pairs thy tycons classes =

  let

    val alg = Sign.classes_of thy

    fun domain_sorts tycon = Sorts.mg_domain alg tycon o single

    fun add_class tycon class =

      cons (class, domain_sorts tycon class)

      handle Sorts.CLASS_ERROR _ => I

    fun try_classes tycon = (tycon, fold (add_class tycon) classes [])

  in map try_classes tycons end

(*Proving one (tycon, class) membership may require proving others, so iterate.*)

fun iter_type_class_pairs _ _ [] = ([], [])

  | iter_type_class_pairs thy tycons classes =

      let

        fun maybe_insert_class s =

          (s <> type_class andalso not (member (op =) classes s))

          ? insert (op =) s

        val cpairs = type_class_pairs thy tycons classes

        val newclasses =

          [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs

        val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses

      in (classes' @ classes, union (op =) cpairs' cpairs) end

fun make_arity_clauses thy tycons =

  iter_type_class_pairs thy tycons ##> multi_arity_clause

(** Isabelle class relations **)

type class_rel_clause =

  {name : string,

   subclass : name,

   superclass : name}

(* Generate all pairs (sub, super) such that sub is a proper subclass of super

   in theory "thy". *)

fun class_pairs _ [] _ = []

  | class_pairs thy subs supers =

      let

        val class_less = Sorts.class_less (Sign.classes_of thy)

        fun add_super sub super = class_less (sub, super) ? cons (sub, super)

        fun add_supers sub = fold (add_super sub) supers

      in fold add_supers subs [] end

fun make_class_rel_clause (sub, super) =

  {name = sub ^ "_" ^ super, subclass = `make_type_class sub,

   superclass = `make_type_class super}

fun make_class_rel_clauses thy subs supers =

  map make_class_rel_clause (class_pairs thy subs supers)

datatype combterm =

  CombConst of name * typ * typ list |

  CombVar of name * typ |

  CombApp of combterm * combterm |

  CombAbs of (name * typ) * combterm

fun combtyp_of (CombConst (_, T, _)) = T

  | combtyp_of (CombVar (_, T)) = T

  | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))

  | combtyp_of (CombAbs ((_, T), tm)) = T --> combtyp_of tm

(*gets the head of a combinator application, along with the list of arguments*)

fun strip_combterm_comb u =

  let

    fun stripc (CombApp (t, u), ts) = stripc (t, u :: ts)

      | stripc x = x

  in stripc (u, []) end

fun atyps_of T = fold_atyps (insert (op =)) T []

fun new_skolem_const_name s num_T_args =

  [new_skolem_const_prefix, s, string_of_int num_T_args]

  |> space_implode Long_Name.separator

(* Converts a term (with combinators) into a combterm. Also accumulates sort

   infomation. *)

fun combterm_from_term thy bs (P $ Q) =

    let

      val (P', P_atomics_Ts) = combterm_from_term thy bs P

      val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q

    in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end

  | combterm_from_term thy _ (Const (c, T)) =

    let

      val tvar_list =

        (if String.isPrefix old_skolem_const_prefix c then

           [] |> Term.add_tvarsT T |> map TVar

         else

           (c, T) |> Sign.const_typargs thy)

      val c' = CombConst (`make_fixed_const c, T, tvar_list)

    in (c', atyps_of T) end

  | combterm_from_term _ _ (Free (v, T)) =

    (CombConst (`make_fixed_var v, T, []), atyps_of T)

  | combterm_from_term _ _ (Var (v as (s, _), T)) =

    (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then

       let

         val Ts = T |> strip_type |> swap |> op ::

         val s' = new_skolem_const_name s (length Ts)

       in CombConst (`make_fixed_const s', T, Ts) end

     else

       CombVar ((make_schematic_var v, s), T), atyps_of T)

  | combterm_from_term _ bs (Bound j) =

    nth bs j

    |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))

  | combterm_from_term thy bs (Abs (s, T, t)) =

    let

      fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string

      val s = vary s

      val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t

    in

      (CombAbs ((`make_bound_var s, T), tm),

       union (op =) atomic_Ts (atyps_of T))

    end

datatype locality =

  General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |

  Chained

(* (quasi-)underapproximation of the truth *)

fun is_locality_global Local = false

  | is_locality_global Assum = false

  | is_locality_global Chained = false

  | is_locality_global _ = true

datatype order = First_Order | Higher_Order

datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic

datatype type_level =

  All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |

  No_Types

datatype type_heaviness = Heavyweight | Lightweight

datatype type_enc =

  Simple_Types of order * type_level |

  Preds of polymorphism * type_level * type_heaviness |

  Tags of polymorphism * type_level * type_heaviness

fun try_unsuffixes ss s =

  fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE

fun type_enc_from_string s =

  (case try (unprefix "poly_") s of

     SOME s => (SOME Polymorphic, s)

   | NONE =>

     case try (unprefix "mono_") s of

       SOME s => (SOME Monomorphic, s)

     | NONE =>

       case try (unprefix "mangled_") s of

         SOME s => (SOME Mangled_Monomorphic, s)

       | NONE => (NONE, s))

  ||> (fn s =>

          (* "_query" and "_bang" are for the ASCII-challenged Metis and

             Mirabelle. *)

          case try_unsuffixes ["?", "_query"] s of

            SOME s => (Noninf_Nonmono_Types, s)

          | NONE =>

            case try_unsuffixes ["!", "_bang"] s of

              SOME s => (Fin_Nonmono_Types, s)

            | NONE => (All_Types, s))

  ||> apsnd (fn s =>

                case try (unsuffix "_heavy") s of

                  SOME s => (Heavyweight, s)

                | NONE => (Lightweight, s))

  |> (fn (poly, (level, (heaviness, core))) =>

         case (core, (poly, level, heaviness)) of

           ("simple", (NONE, _, Lightweight)) =>

           Simple_Types (First_Order, level)

         | ("simple_higher", (NONE, _, Lightweight)) =>

           if level = Noninf_Nonmono_Types then raise Same.SAME

           else Simple_Types (Higher_Order, level)

         | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)

         | ("tags", (SOME Polymorphic, _, _)) =>

           Tags (Polymorphic, level, heaviness)

         | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)

         | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>

           Preds (poly, Const_Arg_Types, Lightweight)

         | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>

           Preds (Polymorphic, No_Types, Lightweight)

         | _ => raise Same.SAME)

  handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")

fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true

  | is_type_enc_higher_order _ = false

fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic

  | polymorphism_of_type_enc (Preds (poly, _, _)) = poly

  | polymorphism_of_type_enc (Tags (poly, _, _)) = poly

fun level_of_type_enc (Simple_Types (_, level)) = level

  | level_of_type_enc (Preds (_, level, _)) = level

  | level_of_type_enc (Tags (_, level, _)) = level

fun heaviness_of_type_enc (Simple_Types _) = Heavyweight

  | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness

  | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness

fun is_type_level_virtually_sound level =

  level = All_Types orelse level = Noninf_Nonmono_Types

val is_type_enc_virtually_sound =

  is_type_level_virtually_sound o level_of_type_enc

fun is_type_level_fairly_sound level =

  is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types

val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc

fun choose_format formats (Simple_Types (order, level)) =

    if member (op =) formats THF then

      (THF, Simple_Types (order, level))

    else if member (op =) formats TFF then

      (TFF, Simple_Types (First_Order, level))

    else

      choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))

  | choose_format formats type_enc =

    (case hd formats of

       CNF_UEQ =>

       (CNF_UEQ, case type_enc of

                   Preds stuff =>

                   (if is_type_enc_fairly_sound type_enc then Tags else Preds)

                       stuff

                 | _ => type_enc)

     | format => (format, type_enc))

type translated_formula =

  {name : string,

   locality : locality,

   kind : formula_kind,

   combformula : (name, typ, combterm) formula,

   atomic_types : typ list}

fun update_combformula f ({name, locality, kind, combformula, atomic_types}

                          : translated_formula) =

  {name = name, locality = locality, kind = kind, combformula = f combformula,

   atomic_types = atomic_types} : translated_formula

fun fact_lift f ({combformula, ...} : translated_formula) = f combformula

val type_instance = Sign.typ_instance o Proof_Context.theory_of

fun insert_type ctxt get_T x xs =

  let val T = get_T x in

    if exists (curry (type_instance ctxt) T o get_T) xs then xs

    else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs

  end

(* The Booleans indicate whether all type arguments should be kept. *)

datatype type_arg_policy =

  Explicit_Type_Args of bool |

  Mangled_Type_Args of bool |

  No_Type_Args

fun should_drop_arg_type_args (Simple_Types _) =

    false (* since TFF doesn't support overloading *)

  | should_drop_arg_type_args type_enc =

    level_of_type_enc type_enc = All_Types andalso

    heaviness_of_type_enc type_enc = Heavyweight

fun type_arg_policy type_enc s =

  if s = type_tag_name then

    (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then

       Mangled_Type_Args

     else

       Explicit_Type_Args) false

  else case type_enc of

    Tags (_, All_Types, Heavyweight) => No_Type_Args

  | _ =>

    if level_of_type_enc type_enc = No_Types orelse

       s = @{const_name HOL.eq} orelse

       (s = app_op_name andalso

        level_of_type_enc type_enc = Const_Arg_Types) then

      No_Type_Args

    else

      should_drop_arg_type_args type_enc

      |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then

            Mangled_Type_Args

          else

            Explicit_Type_Args)

(* Make literals for sorted type variables. *)

fun generic_add_sorts_on_type (_, []) = I

  | generic_add_sorts_on_type ((x, i), s :: ss) =

    generic_add_sorts_on_type ((x, i), ss)

    #> (if s = the_single @{sort HOL.type} then

          I

        else if i = ~1 then

          insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))

        else

          insert (op =) (TyLitVar (`make_type_class s,

                                   (make_schematic_type_var (x, i), x))))

fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)

  | add_sorts_on_tfree _ = I

fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z

  | add_sorts_on_tvar _ = I

fun type_literals_for_types type_enc add_sorts_on_typ Ts =

  [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts

fun mk_aconns c phis =

  let val (phis', phi') = split_last phis in

    fold_rev (mk_aconn c) phis' phi'

  end

fun mk_ahorn [] phi = phi

  | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])

fun mk_aquant _ [] phi = phi

  | mk_aquant q xs (phi as AQuant (q', xs', phi')) =

    if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)

  | mk_aquant q xs phi = AQuant (q, xs, phi)

fun close_universally atom_vars phi =

  let

    fun formula_vars bounds (AQuant (_, xs, phi)) =

        formula_vars (map fst xs @ bounds) phi

      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis

      | formula_vars bounds (AAtom tm) =

        union (op =) (atom_vars tm []

                      |> filter_out (member (op =) bounds o fst))

  in mk_aquant AForall (formula_vars [] phi []) phi end

fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]

  | combterm_vars (CombConst _) = I

  | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)

  | combterm_vars (CombAbs (_, tm)) = combterm_vars tm

fun close_combformula_universally phi = close_universally combterm_vars phi

fun term_vars bounds (ATerm (name as (s, _), tms)) =

    (is_tptp_variable s andalso not (member (op =) bounds name))

    ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms

  | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm

fun close_formula_universally phi = close_universally (term_vars []) phi

val homo_infinite_type_name = @{type_name ind} (* any infinite type *)

val homo_infinite_type = Type (homo_infinite_type_name, [])

fun ho_term_from_typ format type_enc =

  let

    fun term (Type (s, Ts)) =

      ATerm (case (is_type_enc_higher_order type_enc, s) of

               (true, @{type_name bool}) => `I tptp_bool_type

             | (true, @{type_name fun}) => `I tptp_fun_type

             | _ => if s = homo_infinite_type_name andalso

                       (format = TFF orelse format = THF) then

                      `I tptp_individual_type

                    else

                      `make_fixed_type_const s,

             map term Ts)

    | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])

    | term (TVar ((x as (s, _)), _)) =

      ATerm ((make_schematic_type_var x, s), [])

  in term end

fun ho_term_for_type_arg format type_enc T =

  if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)

(* This shouldn't clash with anything else. *)

val mangled_type_sep = "\000"

fun generic_mangled_type_name f (ATerm (name, [])) = f name

  | generic_mangled_type_name f (ATerm (name, tys)) =

    f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)

    ^ ")"

  | generic_mangled_type_name f _ = raise Fail "unexpected type abstraction"

val bool_atype = AType (`I tptp_bool_type)

fun make_simple_type s =

  if s = tptp_bool_type orelse s = tptp_fun_type orelse

     s = tptp_individual_type then

    s

  else

    simple_type_prefix ^ ascii_of s

fun ho_type_from_ho_term type_enc pred_sym ary =

  let

    fun to_atype ty =

      AType ((make_simple_type (generic_mangled_type_name fst ty),

              generic_mangled_type_name snd ty))

    fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))

    fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty

      | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys

      | to_fo ary _ = raise Fail "unexpected type abstraction"

    fun to_ho (ty as ATerm ((s, _), tys)) =

        if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty

      | to_ho _ = raise Fail "unexpected type abstraction"

  in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end

fun ho_type_from_typ format type_enc pred_sym ary =

  ho_type_from_ho_term type_enc pred_sym ary

  o ho_term_from_typ format type_enc

fun mangled_const_name format type_enc T_args (s, s') =

  let

    val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)

    fun type_suffix f g =

      fold_rev (curry (op ^) o g o prefix mangled_type_sep

                o generic_mangled_type_name f) ty_args ""

  in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end

val parse_mangled_ident =

  Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode

fun parse_mangled_type x =

  (parse_mangled_ident

   -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")

                    [] >> ATerm) x

and parse_mangled_types x =

  (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x

fun unmangled_type s =

  s |> suffix ")" |> raw_explode

    |> Scan.finite Symbol.stopper

           (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^

                                                quote s)) parse_mangled_type))

    |> fst

val unmangled_const_name = space_explode mangled_type_sep #> hd

fun unmangled_const s =

  let val ss = space_explode mangled_type_sep s in

    (hd ss, map unmangled_type (tl ss))

  end

fun introduce_proxies type_enc =

  let

    fun intro top_level (CombApp (tm1, tm2)) =

        CombApp (intro top_level tm1, intro false tm2)

      | intro top_level (CombConst (name as (s, _), T, T_args)) =

        (case proxify_const s of

           SOME proxy_base =>

           if top_level orelse is_type_enc_higher_order type_enc then

             case (top_level, s) of

               (_, "c_False") => (`I tptp_false, [])

             | (_, "c_True") => (`I tptp_true, [])

             | (false, "c_Not") => (`I tptp_not, [])

             | (false, "c_conj") => (`I tptp_and, [])

             | (false, "c_disj") => (`I tptp_or, [])

             | (false, "c_implies") => (`I tptp_implies, [])

             | (false, "c_All") => (`I tptp_ho_forall, [])

             | (false, "c_Ex") => (`I tptp_ho_exists, [])

             | (false, s) =>

               if is_tptp_equal s then (`I tptp_equal, [])

               else (proxy_base |>> prefix const_prefix, T_args)

             | _ => (name, [])

           else

             (proxy_base |>> prefix const_prefix, T_args)

          | NONE => (name, T_args))

        |> (fn (name, T_args) => CombConst (name, T, T_args))

      | intro _ (CombAbs (bound, tm)) = CombAbs (bound, intro false tm)

      | intro _ tm = tm

  in intro true end

fun combformula_from_prop thy type_enc eq_as_iff =

  let

    fun do_term bs t atomic_types =

      combterm_from_term thy bs (Envir.eta_contract t)

      |>> (introduce_proxies type_enc #> AAtom)

      ||> union (op =) atomic_types

    fun do_quant bs q s T t' =

      let val s = singleton (Name.variant_list (map fst bs)) s in

        do_formula ((s, T) :: bs) t'

        #>> mk_aquant q [(`make_bound_var s, SOME T)]

      end

    and do_conn bs c t1 t2 =

      do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c)

    and do_formula bs t =

      case t of

        @{const Trueprop} $ t1 => do_formula bs t1

      | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot

      | Const (@{const_name All}, _) $ Abs (s, T, t') =>

        do_quant bs AForall s T t'

      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>

        do_quant bs AExists s T t'

      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2

      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2

      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2

      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>

        if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t

      | _ => do_term bs t

  in do_formula [] end

fun presimplify_term _ [] t = t

  | presimplify_term ctxt presimp_consts t =

    t |> exists_Const (member (op =) presimp_consts o fst) t

         ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)

            #> Meson.presimplify ctxt

            #> prop_of)

fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j

fun conceal_bounds Ts t =

  subst_bounds (map (Free o apfst concealed_bound_name)

                    (0 upto length Ts - 1 ~~ Ts), t)

fun reveal_bounds Ts =

  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))

                    (0 upto length Ts - 1 ~~ Ts))

fun is_fun_equality (@{const_name HOL.eq},

                     Type (_, [Type (@{type_name fun}, _), _])) = true

  | is_fun_equality _ = false

fun extensionalize_term ctxt t =

  if exists_Const is_fun_equality t then

    let val thy = Proof_Context.theory_of ctxt in

      t |> cterm_of thy |> Meson.extensionalize_conv ctxt

        |> prop_of |> Logic.dest_equals |> snd

    end

  else

    t

fun process_abstractions_in_term ctxt type_enc kind t =

  let val thy = Proof_Context.theory_of ctxt in

    if Meson.is_fol_term thy t then

      t

    else

      let

        fun aux Ts t =

          case t of

            @{const Not} $ t1 => @{const Not} $ aux Ts t1

          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>

            t0 $ Abs (s, T, aux (T :: Ts) t')

          | (t0 as Const (@{const_name All}, _)) $ t1 =>

            aux Ts (t0 $ eta_expand Ts t1 1)

          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>

            t0 $ Abs (s, T, aux (T :: Ts) t')

          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>

            aux Ts (t0 $ eta_expand Ts t1 1)

          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))

              $ t1 $ t2 =>

            t0 $ aux Ts t1 $ aux Ts t2

          | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then

                   t

                 else if is_type_enc_higher_order type_enc then

                   t |> Envir.eta_contract

                 else

                   t |> conceal_bounds Ts

                     |> Envir.eta_contract

                     |> cterm_of thy

                     |> Meson_Clausify.introduce_combinators_in_cterm

                     |> prop_of |> Logic.dest_equals |> snd

                     |> reveal_bounds Ts

        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single

      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end

      handle THM _ =>

             (* A type variable of sort "{}" will make abstraction fail. *)

             if kind = Conjecture then HOLogic.false_const

             else HOLogic.true_const

  end

(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the

   same in Sledgehammer to prevent the discovery of unreplayable proofs. *)

fun freeze_term t =

  let

    fun aux (t $ u) = aux t $ aux u

      | aux (Abs (s, T, t)) = Abs (s, T, aux t)

      | aux (Var ((s, i), T)) =

        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)

      | aux t = t

  in t |> exists_subterm is_Var t ? aux end

fun preprocess_prop ctxt type_enc presimp_consts kind t =

  let

    val thy = Proof_Context.theory_of ctxt

    val t = t |> Envir.beta_eta_contract

              |> transform_elim_prop

              |> Object_Logic.atomize_term thy

    val need_trueprop = (fastype_of t = @{typ bool})

  in

    t |> need_trueprop ? HOLogic.mk_Trueprop

      |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []

      |> extensionalize_term ctxt

      |> presimplify_term ctxt presimp_consts

      |> perhaps (try (HOLogic.dest_Trueprop))

      |> process_abstractions_in_term ctxt type_enc kind

  end

(* making fact and conjecture formulas *)

fun make_formula thy type_enc eq_as_iff name loc kind t =

  let

    val (combformula, atomic_types) =

      combformula_from_prop thy type_enc eq_as_iff t []

  in

    {name = name, locality = loc, kind = kind, combformula = combformula,

     atomic_types = atomic_types}

  end

fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts

              ((name, loc), t) =

  let val thy = Proof_Context.theory_of ctxt in

    case t |> preproc ? preprocess_prop ctxt type_enc presimp_consts Axiom

           |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name

                           loc Axiom of

      formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>

      if s = tptp_true then NONE else SOME formula

    | formula => SOME formula

  end

fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =

  let

    val thy = Proof_Context.theory_of ctxt