(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_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 fo_term = 'a ATP_Problem.fo_term

  type format = ATP_Problem.format

  type formula_kind = ATP_Problem.formula_kind

  type 'a problem = 'a ATP_Problem.problem

  type name = string * string

  datatype type_literal =

    TyLitVar of name * name |

    TyLitFree of name * name

  datatype arity_literal =

    TConsLit of name * name * name list |

    TVarLit of name * name

  type arity_clause =

    {name: string,

     prem_lits: arity_literal list,

     concl_lits: arity_literal}

  type class_rel_clause =

    {name: string,

     subclass: name,

     superclass: name}

  datatype combterm =

    CombConst of name * typ * typ list |

    CombVar of name * typ |

    CombApp of combterm * combterm

  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained

  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic

  datatype type_level =

    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types

  datatype type_heaviness = Heavy | Light

  datatype type_system =

    Simple_Types of type_level |

    Preds of polymorphism * type_level * type_heaviness |

    Tags of polymorphism * type_level * type_heaviness

  type translated_formula

  val type_tag_name : string

  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 fact_prefix : string

  val conjecture_prefix : string

  val helper_prefix : string

  val typed_helper_suffix : string

  val predicator_name : string

  val app_op_name : string

  val type_pred_name : string

  val simple_type_prefix : string

  val ascii_of: string -> string

  val unascii_of: string -> string

  val strip_prefix_and_unascii : string -> string -> string option

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

  val invert_const: string -> string

  val unproxify_const: string -> string

  val make_bound_var : string -> string

  val make_schematic_var : string * int -> string

  val make_fixed_var : string -> string

  val make_schematic_type_var : string * int -> string

  val make_fixed_type_var : string -> string

  val make_fixed_const : string -> string

  val make_fixed_type_const : string -> string

  val make_type_class : string -> string

  val make_arity_clauses :

    theory -> string list -> class list -> class list * arity_clause list

  val make_class_rel_clauses :

    theory -> class list -> class list -> class_rel_clause list

  val combtyp_of : combterm -> typ

  val strip_combterm_comb : combterm -> combterm * combterm list

  val atyps_of : typ -> typ list

  val combterm_from_term :

    theory -> (string * typ) list -> term -> combterm * typ list

  val is_locality_global : locality -> bool

  val type_sys_from_string : string -> type_system

  val polymorphism_of_type_sys : type_system -> polymorphism

  val level_of_type_sys : type_system -> type_level

  val is_type_sys_virtually_sound : type_system -> bool

  val is_type_sys_fairly_sound : type_system -> bool

  val raw_type_literals_for_types : typ list -> type_literal list

  val unmangled_const : string -> string * string fo_term list

  val translate_atp_fact :

    Proof.context -> format -> type_system -> bool -> (string * locality) * thm

    -> translated_formula option * ((string * locality) * thm)

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

  val tfree_classes_of_terms : term list -> string list

  val tvar_classes_of_terms : term list -> string list

  val type_consts_of_terms : theory -> term list -> string list

  val prepare_atp_problem :

    Proof.context -> format -> formula_kind -> formula_kind -> type_system

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

    -> (translated_formula option * ((string * 'a) * thm)) list

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

       * (string * 'a) 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

(* FIXME: avoid *)

fun union_all xss = fold (union (op =)) xss []

(* 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 type_tag_name = "ti"

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 sym_formula_prefix = "sym_"

val fact_prefix = "fact_"

val conjecture_prefix = "conj_"

val helper_prefix = "help_"

val class_rel_clause_prefix = "crel_";

val arity_clause_prefix = "arity_"

val tfree_clause_prefix = "tfree_"

val typed_helper_suffix = "_T"

val untyped_helper_suffix = "_U"

val predicator_name = "hBOOL"

val app_op_name = "hAPP"

val type_pred_name = "is"

val simple_type_prefix = "ty_"

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

  [("c_False",

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

   ("c_True", (@{const_name True}, (0, ("fTrue", @{const_name ATP.fTrue})))),

   ("c_Not", (@{const_name Not}, (1, ("fNot", @{const_name ATP.fNot})))),

   ("c_conj", (@{const_name conj}, (2, ("fconj", @{const_name ATP.fconj})))),

   ("c_disj", (@{const_name disj}, (2, ("fdisj", @{const_name ATP.fdisj})))),

   ("c_implies",

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

   ("equal",

    (@{const_name HOL.eq}, (2, ("fequal", @{const_name ATP.fequal}))))]

val proxify_const = AList.lookup (op =) proxies #> Option.map 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 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) proxies

(* 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, (_, (_, metis)))) => Symtab.update (metis, isa)) proxies

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

(*Remove the initial ' character from a type variable, if it is present*)

fun trim_type_var s =

  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)

  else raise Fail ("trim_type: Malformed type variable encountered: " ^ s)

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 (trim_type_var x, i))

fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x))

(* HOL.eq MUST BE "equal" because it's built into ATPs. *)

fun make_fixed_const @{const_name HOL.eq} = "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

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

fun pack_sort (_,[])  = []

  | pack_sort (tvar, "HOL.type" :: srt) =

    pack_sort (tvar, srt) (* IGNORE sort "type" *)

  | pack_sort (tvar, cls :: srt) =

    (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt)

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 = map TVarLit (union_all (map pack_sort tvars_srts)),

     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 ^ "_" ^ class ^ "_" ^ string_of_int n, ar) ::

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

      else

          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ 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 val cpairs = type_class_pairs thy tycons classes

          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))

            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS

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

      in (union (op =) 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

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

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

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

(*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 _ _ (Abs _) = raise Fail "HOL clause: Abs"

datatype locality = General | 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 polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic

datatype type_level =

  All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types

datatype type_heaviness = Heavy | Light

datatype type_system =

  Simple_Types of 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_sys_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 Mirabelle. *)

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

            SOME s => (Nonmonotonic_Types, s)

          | NONE =>

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

              SOME s => (Finite_Types, s)

            | NONE => (All_Types, s))

  ||> apsnd (fn s =>

                case try (unsuffix "_heavy") s of

                  SOME s => (Heavy, s)

                | NONE => (Light, s))

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

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

           ("simple", (NONE, _, Light)) => Simple_Types level

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

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

           Tags (Polymorphic, All_Types, heaviness)

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

           (* The actual light encoding is very unsound. *)

           Tags (Polymorphic, level, Heavy)

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

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

           Preds (poly, Const_Arg_Types, Light)

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

           Preds (Polymorphic, No_Types, Light)

         | _ => raise Same.SAME)

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

fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic

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

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

fun level_of_type_sys (Simple_Types level) = level

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

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

fun heaviness_of_type_sys (Simple_Types _) = Heavy

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

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

fun is_type_level_virtually_sound level =

  level = All_Types orelse level = Nonmonotonic_Types

val is_type_sys_virtually_sound =

  is_type_level_virtually_sound o level_of_type_sys

fun is_type_level_fairly_sound level =

  is_type_level_virtually_sound level orelse level = Finite_Types

val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys

fun is_setting_higher_order THF (Simple_Types _) = true

  | is_setting_higher_order _ _ = false

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_sys =

    level_of_type_sys type_sys = All_Types andalso

    heaviness_of_type_sys type_sys = Heavy

fun general_type_arg_policy type_sys =

  if level_of_type_sys type_sys = No_Types then

    No_Type_Args

  else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then

    Mangled_Type_Args (should_drop_arg_type_args type_sys)

  else

    Explicit_Type_Args (should_drop_arg_type_args type_sys)

fun type_arg_policy type_sys s =

  if s = @{const_name HOL.eq} orelse

     (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then

    No_Type_Args

  else

    general_type_arg_policy type_sys

(*Make literals for sorted type variables*)

fun sorts_on_typs_aux (_, [])   = []

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

      let val sorts = sorts_on_typs_aux ((x,i), ss)

      in

          if s = the_single @{sort HOL.type} then sorts

          else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts

          else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts

      end;

fun sorts_on_typs (TFree (a, s)) = sorts_on_typs_aux ((a, ~1), s)

  | sorts_on_typs (TVar (v, s)) = sorts_on_typs_aux (v, s)

  | sorts_on_typs _ = raise Fail "expected \"TVar\" or \"TFree\""

(*Given a list of sorted type variables, return a list of type literals.*)

val raw_type_literals_for_types = union_all o map sorts_on_typs

fun type_literals_for_types format type_sys kind Ts =

  if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then

    []

  else

    Ts |> raw_type_literals_for_types

       |> filter (fn TyLitVar _ => kind <> Conjecture

                   | TyLitFree _ => kind = Conjecture)

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)

fun close_combformula_universally phi = close_universally combterm_vars phi

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

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

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 fo_term_from_typ higher_order =

  let

    fun term (Type (s, Ts)) =

      ATerm (case (higher_order, s) of

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

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

             | _ => if s = homo_infinite_type_name 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

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

    ^ ")"

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_fo_term higher_order 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

    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

  in if higher_order then to_ho else to_fo ary end

fun mangled_type higher_order pred_sym ary =

  ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order

fun mangled_const_name T_args (s, s') =

  let

    val ty_args = map (fo_term_from_typ false) T_args

    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 format type_sys =

  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_setting_higher_order format type_sys 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, 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 _ tm = tm

  in intro true end

fun combformula_from_prop thy format type_sys eq_as_iff =

  let

    fun do_term bs t atomic_types =

      combterm_from_term thy bs (Envir.eta_contract t)

      |>> (introduce_proxies format type_sys #> AAtom)

      ||> union (op =) atomic_types

    fun do_quant bs q s T t' =

      let val s = Name.variant (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 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 ctxt =

  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 extensionalize_term ctxt t =

  let val thy = Proof_Context.theory_of ctxt in

    t |> cterm_of thy |> Meson.extensionalize_conv ctxt

      |> prop_of |> Logic.dest_equals |> snd

  end

fun introduce_combinators_in_term ctxt 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

                   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

(* making fact and conjecture formulas *)

fun make_formula ctxt format type_sys eq_as_iff presimp name loc 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})

    val t = t |> need_trueprop ? HOLogic.mk_Trueprop

              |> Raw_Simplifier.rewrite_term thy

                     (Meson.unfold_set_const_simps ctxt) []

              |> extensionalize_term ctxt

              |> presimp ? presimplify_term ctxt

              |> perhaps (try (HOLogic.dest_Trueprop))

              |> introduce_combinators_in_term ctxt kind

              |> kind <> Axiom ? freeze_term

    val (combformula, atomic_types) =

      combformula_from_prop thy format type_sys eq_as_iff t []

  in

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

     atomic_types = atomic_types}

  end

fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp

              ((name, loc), t) =

  case (keep_trivial,

        make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of

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

    if s = tptp_true then NONE else SOME formula

  | (_, formula) => SOME formula

fun make_conjecture ctxt format prem_kind type_sys ts =

  let val last = length ts - 1 in

    map2 (fn j => fn t =>

             let

               val (kind, maybe_negate) =

                 if j = last then

                   (Conjecture, I)

                 else

                   (prem_kind,

                    if prem_kind = Conjecture then update_combformula mk_anot

                    else I)

              in

                t |> make_formula ctxt format type_sys true true

                                  (string_of_int j) General kind

                  |> maybe_negate

              end)

         (0 upto last) ts

  end

(** Finite and infinite type inference **)

fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)

  | deep_freeze_atyp T = T

val deep_freeze_type = map_atyps deep_freeze_atyp

(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are

   dangerous because their "exhaust" properties can easily lead to unsound ATP

   proofs. On the other hand, all HOL infinite types can be given the same

   models in first-order logic (via Löwenheim-Skolem). *)

fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =

    exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts

  | should_encode_type _ _ All_Types _ = true

  | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T

  | should_encode_type _ _ _ _ = false

fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))

                             should_predicate_on_var T =

    (heaviness = Heavy orelse should_predicate_on_var ()) andalso

    should_encode_type ctxt nonmono_Ts level T

  | should_predicate_on_type _ _ _ _ _ = false

fun is_var_or_bound_var (CombConst ((s, _), _, _)) =

    String.isPrefix bound_var_prefix s

  | is_var_or_bound_var (CombVar _) = true

  | is_var_or_bound_var _ = false

datatype tag_site = Top_Level | Eq_Arg | Elsewhere

fun should_tag_with_type _ _ _ Top_Level _ _ = false

  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =

    (case heaviness of

       Heavy => should_encode_type ctxt nonmono_Ts level T

     | Light =>

       case (site, is_var_or_bound_var u) of

         (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T

       | _ => false)

  | should_tag_with_type _ _ _ _ _ _ = false

fun homogenized_type ctxt nonmono_Ts level =

  let

    val should_encode = should_encode_type ctxt nonmono_Ts level

    fun homo 0 T = if should_encode T then T else homo_infinite_type

      | homo ary (Type (@{type_name fun}, [T1, T2])) =

        homo 0 T1 --> homo (ary - 1) T2

      | homo _ _ = raise Fail "expected function type"

  in homo end

(** "hBOOL" and "hAPP" **)

type sym_info =

  {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}

fun add_combterm_syms_to_table ctxt explicit_apply =

  let

    fun consider_var_arity const_T var_T max_ary =

      let

        fun iter ary T =

          if ary = max_ary orelse type_instance ctxt (var_T, T) then ary

          else iter (ary + 1) (range_type T)

      in iter 0 const_T end

    fun add top_level tm (accum as (ho_var_Ts, sym_tab)) =

      let val (head, args) = strip_combterm_comb tm in

        (case head of

           CombConst ((s, _), T, _) =>

           if String.isPrefix bound_var_prefix s then

             if explicit_apply = NONE andalso can dest_funT T then

               let

                 fun repair_min_arity {pred_sym, min_ary, max_ary, types} =

                   {pred_sym = pred_sym,

                    min_ary =

                      fold (fn T' => consider_var_arity T' T) types min_ary,

                    max_ary = max_ary, types = types}

                 val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T

               in

                 if pointer_eq (ho_var_Ts', ho_var_Ts) then accum

                 else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)

               end

             else

               accum