src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
author blanchet
Sun May 01 18:37:23 2011 +0200 (2011-05-01)
changeset 42521 02df3b78a438
parent 42520 d1f7c4a01dbe
child 42522 413b56894f82
permissions -rw-r--r--
get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Translation of HOL to FOL for Sledgehammer.
     7 *)
     8 
     9 signature SLEDGEHAMMER_ATP_TRANSLATE =
    10 sig
    11   type 'a fo_term = 'a ATP_Problem.fo_term
    12   type 'a problem = 'a ATP_Problem.problem
    13   type translated_formula
    14 
    15   datatype type_system =
    16     Tags of bool |
    17     Args |
    18     Mangled |
    19     No_Types
    20 
    21   val risky_overloaded_args : bool Unsynchronized.ref
    22   val fact_prefix : string
    23   val conjecture_prefix : string
    24   val is_type_system_sound : type_system -> bool
    25   val type_system_types_dangerous_types : type_system -> bool
    26   val num_atp_type_args : theory -> type_system -> string -> int
    27   val translate_atp_fact :
    28     Proof.context -> bool -> (string * 'a) * thm
    29     -> translated_formula option * ((string * 'a) * thm)
    30   val unmangled_const : string -> string * string fo_term list
    31   val prepare_atp_problem :
    32     Proof.context -> bool -> type_system -> bool -> term list -> term
    33     -> (translated_formula option * ((string * 'a) * thm)) list
    34     -> string problem * string Symtab.table * int * (string * 'a) list vector
    35   val atp_problem_weights : string problem -> (string * real) list
    36 end;
    37 
    38 structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
    39 struct
    40 
    41 open ATP_Problem
    42 open Metis_Translate
    43 open Sledgehammer_Util
    44 
    45 (* FIXME: Remove references once appropriate defaults have been determined
    46    empirically. *)
    47 val risky_overloaded_args = Unsynchronized.ref false
    48 
    49 val fact_prefix = "fact_"
    50 val conjecture_prefix = "conj_"
    51 val helper_prefix = "help_"
    52 val class_rel_clause_prefix = "clrel_";
    53 val arity_clause_prefix = "arity_"
    54 val tfree_prefix = "tfree_"
    55 
    56 (* Freshness almost guaranteed! *)
    57 val sledgehammer_weak_prefix = "Sledgehammer:"
    58 
    59 type translated_formula =
    60   {name: string,
    61    kind: kind,
    62    combformula: (name, combterm) formula,
    63    ctypes_sorts: typ list}
    64 
    65 datatype type_system =
    66   Tags of bool |
    67   Args |
    68   Mangled |
    69   No_Types
    70 
    71 fun is_type_system_sound (Tags true) = true
    72   | is_type_system_sound _ = false
    73 
    74 fun type_system_types_dangerous_types (Tags _) = true
    75   | type_system_types_dangerous_types _ = false
    76 
    77 (* This is an approximation. If it returns "true" for a constant that isn't
    78    overloaded (i.e., that has one uniform definition), needless clutter is
    79    generated; if it returns "false" for an overloaded constant, the ATP gets a
    80    license to do unsound reasoning if the type system is "overloaded_args". *)
    81 fun is_overloaded thy s =
    82   not (s = @{const_name HOL.eq}) andalso
    83   not (s = @{const_name Metis.fequal}) andalso
    84   (not (!risky_overloaded_args) orelse s = @{const_name finite} orelse
    85    length (Defs.specifications_of (Theory.defs_of thy) s) > 1)
    86 
    87 fun needs_type_args thy type_sys s =
    88   case type_sys of
    89     Tags full_types => not full_types andalso is_overloaded thy s
    90   | Args => is_overloaded thy s
    91   | Mangled => true
    92   | No_Types => false
    93 
    94 datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types
    95 
    96 fun type_arg_policy thy type_sys s =
    97   if needs_type_args thy type_sys s then
    98     if type_sys = Mangled then Mangled_Types else Explicit_Type_Args
    99   else
   100     No_Type_Args
   101 
   102 fun num_atp_type_args thy type_sys s =
   103   if type_arg_policy thy type_sys s = Explicit_Type_Args then
   104     num_type_args thy s
   105   else
   106     0
   107 
   108 fun atp_type_literals_for_types type_sys kind Ts =
   109   if type_sys = No_Types then
   110     []
   111   else
   112     Ts |> type_literals_for_types
   113        |> filter (fn TyLitVar _ => kind <> Conjecture
   114                    | TyLitFree _ => kind = Conjecture)
   115 
   116 fun mk_anot phi = AConn (ANot, [phi])
   117 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
   118 fun mk_ahorn [] phi = phi
   119   | mk_ahorn (phi :: phis) psi =
   120     AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
   121 
   122 fun close_universally phi =
   123   let
   124     fun term_vars bounds (ATerm (name as (s, _), tms)) =
   125         (is_atp_variable s andalso not (member (op =) bounds name))
   126           ? insert (op =) name
   127         #> fold (term_vars bounds) tms
   128     fun formula_vars bounds (AQuant (_, xs, phi)) =
   129         formula_vars (xs @ bounds) phi
   130       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   131       | formula_vars bounds (AAtom tm) = term_vars bounds tm
   132   in
   133     case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   134   end
   135 
   136 fun combformula_for_prop thy eq_as_iff =
   137   let
   138     fun do_term bs t ts =
   139       combterm_from_term thy bs (Envir.eta_contract t)
   140       |>> AAtom ||> union (op =) ts
   141     fun do_quant bs q s T t' =
   142       let val s = Name.variant (map fst bs) s in
   143         do_formula ((s, T) :: bs) t'
   144         #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
   145       end
   146     and do_conn bs c t1 t2 =
   147       do_formula bs t1 ##>> do_formula bs t2
   148       #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
   149     and do_formula bs t =
   150       case t of
   151         @{const Not} $ t1 =>
   152         do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
   153       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   154         do_quant bs AForall s T t'
   155       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   156         do_quant bs AExists s T t'
   157       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
   158       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
   159       | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
   160       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   161         if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
   162       | _ => do_term bs t
   163   in do_formula [] end
   164 
   165 val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
   166 
   167 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
   168 fun conceal_bounds Ts t =
   169   subst_bounds (map (Free o apfst concealed_bound_name)
   170                     (0 upto length Ts - 1 ~~ Ts), t)
   171 fun reveal_bounds Ts =
   172   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   173                     (0 upto length Ts - 1 ~~ Ts))
   174 
   175 (* Removes the lambdas from an equation of the form "t = (%x. u)".
   176    (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
   177 fun extensionalize_term t =
   178   let
   179     fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
   180       | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
   181                                         Type (_, [_, res_T])]))
   182                     $ t2 $ Abs (var_s, var_T, t')) =
   183         if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
   184           let val var_t = Var ((var_s, j), var_T) in
   185             Const (s, T' --> T' --> res_T)
   186               $ betapply (t2, var_t) $ subst_bound (var_t, t')
   187             |> aux (j + 1)
   188           end
   189         else
   190           t
   191       | aux _ t = t
   192   in aux (maxidx_of_term t + 1) t end
   193 
   194 fun introduce_combinators_in_term ctxt kind t =
   195   let val thy = Proof_Context.theory_of ctxt in
   196     if Meson.is_fol_term thy t then
   197       t
   198     else
   199       let
   200         fun aux Ts t =
   201           case t of
   202             @{const Not} $ t1 => @{const Not} $ aux Ts t1
   203           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   204             t0 $ Abs (s, T, aux (T :: Ts) t')
   205           | (t0 as Const (@{const_name All}, _)) $ t1 =>
   206             aux Ts (t0 $ eta_expand Ts t1 1)
   207           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   208             t0 $ Abs (s, T, aux (T :: Ts) t')
   209           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   210             aux Ts (t0 $ eta_expand Ts t1 1)
   211           | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   212           | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   213           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   214           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   215               $ t1 $ t2 =>
   216             t0 $ aux Ts t1 $ aux Ts t2
   217           | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   218                    t
   219                  else
   220                    t |> conceal_bounds Ts
   221                      |> Envir.eta_contract
   222                      |> cterm_of thy
   223                      |> Meson_Clausify.introduce_combinators_in_cterm
   224                      |> prop_of |> Logic.dest_equals |> snd
   225                      |> reveal_bounds Ts
   226         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   227       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   228       handle THM _ =>
   229              (* A type variable of sort "{}" will make abstraction fail. *)
   230              if kind = Conjecture then HOLogic.false_const
   231              else HOLogic.true_const
   232   end
   233 
   234 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   235    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
   236 fun freeze_term t =
   237   let
   238     fun aux (t $ u) = aux t $ aux u
   239       | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   240       | aux (Var ((s, i), T)) =
   241         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   242       | aux t = t
   243   in t |> exists_subterm is_Var t ? aux end
   244 
   245 (* making fact and conjecture formulas *)
   246 fun make_formula ctxt eq_as_iff presimp name kind t =
   247   let
   248     val thy = Proof_Context.theory_of ctxt
   249     val t = t |> Envir.beta_eta_contract
   250               |> transform_elim_term
   251               |> Object_Logic.atomize_term thy
   252     val need_trueprop = (fastype_of t = HOLogic.boolT)
   253     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   254               |> extensionalize_term
   255               |> presimp ? presimplify_term thy
   256               |> perhaps (try (HOLogic.dest_Trueprop))
   257               |> introduce_combinators_in_term ctxt kind
   258               |> kind <> Axiom ? freeze_term
   259     val (combformula, ctypes_sorts) = combformula_for_prop thy eq_as_iff t []
   260   in
   261     {name = name, combformula = combformula, kind = kind,
   262      ctypes_sorts = ctypes_sorts}
   263   end
   264 
   265 fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), th) =
   266   case (keep_trivial,
   267         make_formula ctxt eq_as_iff presimp name Axiom (prop_of th)) of
   268     (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
   269     NONE
   270   | (_, formula) => SOME formula
   271 fun make_conjecture ctxt ts =
   272   let val last = length ts - 1 in
   273     map2 (fn j => make_formula ctxt true true (string_of_int j)
   274                                (if j = last then Conjecture else Hypothesis))
   275          (0 upto last) ts
   276   end
   277 
   278 (** Helper facts **)
   279 
   280 fun fold_formula f (AQuant (_, _, phi)) = fold_formula f phi
   281   | fold_formula f (AConn (_, phis)) = fold (fold_formula f) phis
   282   | fold_formula f (AAtom tm) = f tm
   283 
   284 fun count_term (ATerm ((s, _), tms)) =
   285   (if is_atp_variable s then I
   286    else Symtab.map_entry s (Integer.add 1))
   287   #> fold count_term tms
   288 fun count_formula x = fold_formula count_term x
   289 
   290 val init_counters =
   291   metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0)
   292   |> Symtab.make
   293 
   294 fun get_helper_facts ctxt type_sys formulas =
   295   let
   296     val no_dangerous_types = type_system_types_dangerous_types type_sys
   297     val ct = init_counters |> fold count_formula formulas
   298     fun is_used s = the (Symtab.lookup ct s) > 0
   299     fun dub c needs_full_types (th, j) =
   300       ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""),
   301         false), th)
   302     fun make_facts eq_as_iff = map_filter (make_fact ctxt false eq_as_iff false)
   303   in
   304     (metis_helpers
   305      |> filter (is_used o fst)
   306      |> maps (fn (c, (needs_full_types, ths)) =>
   307                  if needs_full_types andalso not no_dangerous_types then
   308                    []
   309                  else
   310                    ths ~~ (1 upto length ths)
   311                    |> map (dub c needs_full_types)
   312                    |> make_facts (not needs_full_types)),
   313      if type_sys = Tags false then
   314        let
   315          fun var s = ATerm (`I s, [])
   316          fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
   317        in
   318          [Fof (helper_prefix ^ ascii_of "ti_ti", Axiom,
   319                AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
   320                |> close_universally, NONE)]
   321        end
   322      else
   323        [])
   324   end
   325 
   326 fun translate_atp_fact ctxt keep_trivial =
   327   `(make_fact ctxt keep_trivial true true)
   328 
   329 fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
   330   let
   331     val thy = Proof_Context.theory_of ctxt
   332     val fact_ts = map (prop_of o snd o snd) rich_facts
   333     val (facts, fact_names) =
   334       rich_facts
   335       |> map_filter (fn (NONE, _) => NONE
   336                       | (SOME fact, (name, _)) => SOME (fact, name))
   337       |> ListPair.unzip
   338     (* Remove existing facts from the conjecture, as this can dramatically
   339        boost an ATP's performance (for some reason). *)
   340     val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
   341     val goal_t = Logic.list_implies (hyp_ts, concl_t)
   342     val all_ts = goal_t :: fact_ts
   343     val subs = tfree_classes_of_terms all_ts
   344     val supers = tvar_classes_of_terms all_ts
   345     val tycons = type_consts_of_terms thy all_ts
   346     val conjs = make_conjecture ctxt (hyp_ts @ [concl_t])
   347     val (supers', arity_clauses) =
   348       if type_sys = No_Types then ([], [])
   349       else make_arity_clauses thy tycons supers
   350     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   351   in
   352     (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
   353   end
   354 
   355 fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t])
   356 
   357 fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   358   | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   359   | fo_term_for_combtyp (CombType (name, tys)) =
   360     ATerm (name, map fo_term_for_combtyp tys)
   361 
   362 fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   363     (true, ATerm (class, [ATerm (name, [])]))
   364   | fo_literal_for_type_literal (TyLitFree (class, name)) =
   365     (true, ATerm (class, [ATerm (name, [])]))
   366 
   367 fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   368 
   369 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
   370    considered dangerous because their "exhaust" properties can easily lead to
   371    unsound ATP proofs. The checks below are an (unsound) approximation of
   372    finiteness. *)
   373 
   374 fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true
   375   | is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) =
   376     is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us
   377   | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false
   378 and is_type_dangerous ctxt (Type (s, Ts)) =
   379     is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts
   380   | is_type_dangerous _ _ = false
   381 and is_type_constr_dangerous ctxt s =
   382   let val thy = Proof_Context.theory_of ctxt in
   383     case Datatype_Data.get_info thy s of
   384       SOME {descr, ...} =>
   385       forall (fn (_, (_, _, constrs)) =>
   386                  forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr
   387     | NONE =>
   388       case Typedef.get_info ctxt s of
   389         ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type
   390       | [] => true
   391   end
   392 
   393 fun is_combtyp_dangerous ctxt (CombType ((s, _), tys)) =
   394     (case strip_prefix_and_unascii type_const_prefix s of
   395        SOME s' => forall (is_combtyp_dangerous ctxt) tys andalso
   396                   is_type_constr_dangerous ctxt (invert_const s')
   397      | NONE => false)
   398   | is_combtyp_dangerous _ _ = false
   399 
   400 fun should_tag_with_type ctxt (Tags full_types) ty =
   401     full_types orelse is_combtyp_dangerous ctxt ty
   402   | should_tag_with_type _ _ _ = false
   403 
   404 val fname_table =
   405   [("c_False", (0, ("c_fFalse", @{const_name Metis.fFalse}))),
   406    ("c_True", (0, ("c_fTrue", @{const_name Metis.fTrue}))),
   407    ("c_Not", (1, ("c_fNot", @{const_name Metis.fNot}))),
   408    ("c_conj", (2, ("c_fconj", @{const_name Metis.fconj}))),
   409    ("c_disj", (2, ("c_fdisj", @{const_name Metis.fdisj}))),
   410    ("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))),
   411    ("equal", (2, ("c_fequal", @{const_name Metis.fequal})))]
   412 
   413 (* We are crossing our fingers that it doesn't clash with anything else. *)
   414 val mangled_type_sep = "\000"
   415 
   416 fun mangled_combtyp f (CombTFree name) = f name
   417   | mangled_combtyp f (CombTVar name) =
   418     f name (* FIXME: shouldn't happen *)
   419     (* raise Fail "impossible schematic type variable" *)
   420   | mangled_combtyp f (CombType (name, tys)) =
   421     "(" ^ commas (map (mangled_combtyp f) tys) ^ ")" ^ f name
   422 
   423 fun mangled_type_suffix f g tys =
   424   fold_rev (curry (op ^) o g o prefix mangled_type_sep o mangled_combtyp f)
   425            tys ""
   426 
   427 val parse_mangled_ident =
   428   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
   429 
   430 fun parse_mangled_type x =
   431   ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")"
   432       -- parse_mangled_ident >> (ATerm o swap)
   433    || parse_mangled_ident >> (ATerm o rpair [])) x
   434 and parse_mangled_types x =
   435   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
   436 
   437 fun unmangled_type s =
   438   s |> suffix ")" |> raw_explode
   439     |> Scan.finite Symbol.stopper
   440            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
   441                                                 quote s)) parse_mangled_type))
   442     |> fst
   443 
   444 fun unmangled_const s =
   445   let val ss = space_explode mangled_type_sep s in
   446     (hd ss, map unmangled_type (tl ss))
   447   end
   448 
   449 fun fo_term_for_combterm ctxt type_sys =
   450   let
   451     val thy = Proof_Context.theory_of ctxt
   452     fun aux top_level u =
   453       let
   454         val (head, args) = strip_combterm_comb u
   455         val (x, ty_args) =
   456           case head of
   457             CombConst (name as (s, s'), _, ty_args) =>
   458             (case AList.lookup (op =) fname_table s of
   459                SOME (n, fname) =>
   460                (if top_level andalso length args = n then
   461                   case s of
   462                     "c_False" => ("$false", s')
   463                   | "c_True" => ("$true", s')
   464                   | _ => name
   465                 else
   466                   fname, [])
   467              | NONE =>
   468                case strip_prefix_and_unascii const_prefix s of
   469                  NONE => (name, ty_args)
   470                | SOME s'' =>
   471                  let val s'' = invert_const s'' in
   472                    case type_arg_policy thy type_sys s'' of
   473                      No_Type_Args => (name, [])
   474                    | Explicit_Type_Args => (name, ty_args)
   475                    | Mangled_Types =>
   476                      ((s ^ mangled_type_suffix fst ascii_of ty_args,
   477                        s' ^ mangled_type_suffix snd I ty_args), [])
   478                  end)
   479           | CombVar (name, _) => (name, [])
   480           | CombApp _ => raise Fail "impossible \"CombApp\""
   481         val t =
   482           ATerm (x, map fo_term_for_combtyp ty_args @ map (aux false) args)
   483         val ty = combtyp_of u
   484     in
   485       t |> (if should_tag_with_type ctxt type_sys ty then
   486               tag_with_type (fo_term_for_combtyp ty)
   487             else
   488               I)
   489     end
   490   in aux true end
   491 
   492 fun formula_for_combformula ctxt type_sys =
   493   let
   494     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   495       | aux (AConn (c, phis)) = AConn (c, map aux phis)
   496       | aux (AAtom tm) = AAtom (fo_term_for_combterm ctxt type_sys tm)
   497   in aux end
   498 
   499 fun formula_for_fact ctxt type_sys
   500                      ({combformula, ctypes_sorts, ...} : translated_formula) =
   501   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   502                 (atp_type_literals_for_types type_sys Axiom ctypes_sorts))
   503            (formula_for_combformula ctxt type_sys combformula)
   504 
   505 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   506    of monomorphization). The TPTP explicitly forbids name clashes, and some of
   507    the remote provers might care. *)
   508 fun problem_line_for_fact ctxt prefix type_sys
   509                           (j, formula as {name, kind, ...}) =
   510   Fof (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
   511        formula_for_fact ctxt type_sys formula, NONE)
   512 
   513 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   514                                                        superclass, ...}) =
   515   let val ty_arg = ATerm (("T", "T"), []) in
   516     Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
   517          AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   518                            AAtom (ATerm (superclass, [ty_arg]))]), NONE)
   519   end
   520 
   521 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   522     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   523   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   524     (false, ATerm (c, [ATerm (sort, [])]))
   525 
   526 fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   527                                                 ...}) =
   528   Fof (arity_clause_prefix ^ ascii_of name, Axiom,
   529        mk_ahorn (map (formula_for_fo_literal o apfst not
   530                       o fo_literal_for_arity_literal) premLits)
   531                 (formula_for_fo_literal
   532                      (fo_literal_for_arity_literal conclLit)), NONE)
   533 
   534 fun problem_line_for_conjecture ctxt type_sys
   535         ({name, kind, combformula, ...} : translated_formula) =
   536   Fof (conjecture_prefix ^ name, kind,
   537        formula_for_combformula ctxt type_sys combformula, NONE)
   538 
   539 fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) =
   540   ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture
   541                |> map fo_literal_for_type_literal
   542 
   543 fun problem_line_for_free_type j lit =
   544   Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit,
   545        NONE)
   546 fun problem_lines_for_free_types type_sys facts =
   547   let
   548     val litss = map (free_type_literals type_sys) facts
   549     val lits = fold (union (op =)) litss []
   550   in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
   551 
   552 (** "hBOOL" and "hAPP" **)
   553 
   554 type sym_info = {min_arity: int, max_arity: int, fun_sym: bool}
   555 
   556 fun consider_term top_level (ATerm ((s, _), ts)) =
   557   (if is_atp_variable s then
   558      I
   559    else
   560      let val n = length ts in
   561        Symtab.map_default
   562            (s, {min_arity = n, max_arity = 0, fun_sym = false})
   563            (fn {min_arity, max_arity, fun_sym} =>
   564                {min_arity = Int.min (n, min_arity),
   565                 max_arity = Int.max (n, max_arity),
   566                 fun_sym = fun_sym orelse not top_level})
   567      end)
   568   #> fold (consider_term (top_level andalso s = type_tag_name)) ts
   569 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   570   | consider_formula (AConn (_, phis)) = fold consider_formula phis
   571   | consider_formula (AAtom tm) = consider_term true tm
   572 
   573 fun consider_problem_line (Fof (_, _, phi, _)) = consider_formula phi
   574 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   575 
   576 (* needed for helper facts if the problem otherwise does not involve equality *)
   577 val equal_entry = ("equal", {min_arity = 2, max_arity = 2, fun_sym = false})
   578 
   579 fun sym_table_for_problem explicit_apply problem =
   580   if explicit_apply then
   581     NONE
   582   else
   583     SOME (Symtab.empty |> Symtab.default equal_entry |> consider_problem problem)
   584 
   585 fun min_arity_of thy type_sys NONE s =
   586     (if s = "equal" orelse s = type_tag_name orelse
   587         String.isPrefix type_const_prefix s orelse
   588         String.isPrefix class_prefix s then
   589        16383 (* large number *)
   590      else case strip_prefix_and_unascii const_prefix s of
   591        SOME s' =>
   592        s' |> unmangled_const |> fst |> invert_const
   593           |> num_atp_type_args thy type_sys
   594      | NONE => 0)
   595   | min_arity_of _ _ (SOME sym_tab) s =
   596     case Symtab.lookup sym_tab s of
   597       SOME ({min_arity, ...} : sym_info) => min_arity
   598     | NONE => 0
   599 
   600 fun full_type_of (ATerm ((s, _), [ty, _])) =
   601     if s = type_tag_name then SOME ty else NONE
   602   | full_type_of _ = NONE
   603 
   604 fun list_hAPP_rev _ t1 [] = t1
   605   | list_hAPP_rev NONE t1 (t2 :: ts2) =
   606     ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
   607   | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   608     case full_type_of t2 of
   609       SOME ty2 =>
   610       let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   611                            [ty2, ty]) in
   612         ATerm (`I "hAPP",
   613                [tag_with_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   614       end
   615     | NONE => list_hAPP_rev NONE t1 (t2 :: ts2)
   616 
   617 fun repair_applications_in_term thy type_sys sym_tab =
   618   let
   619     fun aux opt_ty (ATerm (name as (s, _), ts)) =
   620       if s = type_tag_name then
   621         case ts of
   622           [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   623         | _ => raise Fail "malformed type tag"
   624       else
   625         let
   626           val ts = map (aux NONE) ts
   627           val (ts1, ts2) = chop (min_arity_of thy type_sys sym_tab s) ts
   628         in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   629   in aux NONE end
   630 
   631 fun boolify t = ATerm (`I "hBOOL", [t])
   632 
   633 (* True if the constant ever appears outside of the top-level position in
   634    literals, or if it appears with different arities (e.g., because of different
   635    type instantiations). If false, the constant always receives all of its
   636    arguments and is used as a predicate. *)
   637 fun is_pred_sym NONE s =
   638     s = "equal" orelse s = "$false" orelse s = "$true" orelse
   639     String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
   640   | is_pred_sym (SOME sym_tab) s =
   641     case Symtab.lookup sym_tab s of
   642       SOME {min_arity, max_arity, fun_sym} =>
   643       not fun_sym andalso min_arity = max_arity
   644     | NONE => false
   645 
   646 fun repair_predicates_in_term pred_sym_tab (t as ATerm ((s, _), ts)) =
   647   if s = type_tag_name then
   648     case ts of
   649       [_, t' as ATerm ((s', _), _)] =>
   650       if is_pred_sym pred_sym_tab s' then t' else boolify t
   651     | _ => raise Fail "malformed type tag"
   652   else
   653     t |> not (is_pred_sym pred_sym_tab s) ? boolify
   654 
   655 fun repair_formula thy type_sys sym_tab =
   656   let
   657     val pred_sym_tab = case type_sys of Tags _ => NONE | _ => sym_tab
   658     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   659       | aux (AConn (c, phis)) = AConn (c, map aux phis)
   660       | aux (AAtom tm) =
   661         AAtom (tm |> repair_applications_in_term thy type_sys sym_tab
   662                   |> repair_predicates_in_term pred_sym_tab)
   663   in aux #> close_universally end
   664 
   665 fun repair_problem_line thy type_sys sym_tab (Fof (ident, kind, phi, source)) =
   666   Fof (ident, kind, repair_formula thy type_sys sym_tab phi, source)
   667 fun repair_problem thy = map o apsnd o map oo repair_problem_line thy
   668 
   669 fun dest_Fof (Fof z) = z
   670 
   671 val factsN = "Relevant facts"
   672 val class_relsN = "Class relationships"
   673 val aritiesN = "Arity declarations"
   674 val helpersN = "Helper facts"
   675 val conjsN = "Conjectures"
   676 val free_typesN = "Type variables"
   677 
   678 fun offset_of_heading_in_problem _ [] j = j
   679   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
   680     if heading = needle then j
   681     else offset_of_heading_in_problem needle problem (j + length lines)
   682 
   683 fun prepare_atp_problem ctxt readable_names type_sys explicit_apply hyp_ts
   684                         concl_t facts =
   685   let
   686     val thy = Proof_Context.theory_of ctxt
   687     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
   688       translate_formulas ctxt type_sys hyp_ts concl_t facts
   689     (* Reordering these might or might not confuse the proof reconstruction
   690        code or the SPASS Flotter hack. *)
   691     val problem =
   692       [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
   693                     (0 upto length facts - 1 ~~ facts)),
   694        (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
   695        (aritiesN, map problem_line_for_arity_clause arity_clauses),
   696        (helpersN, []),
   697        (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
   698        (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))]
   699     val sym_tab = sym_table_for_problem explicit_apply problem
   700     val problem = problem |> repair_problem thy type_sys sym_tab
   701     val helper_facts =
   702       get_helper_facts ctxt type_sys (maps (map (#3 o dest_Fof) o snd) problem)
   703     val helper_lines =
   704       helper_facts
   705       |>> map (pair 0
   706                #> problem_line_for_fact ctxt helper_prefix type_sys
   707                #> repair_problem_line thy type_sys sym_tab)
   708       |> op @
   709     val (problem, pool) =
   710       problem |> AList.update (op =) (helpersN, helper_lines)
   711               |> nice_atp_problem readable_names
   712   in
   713     (problem,
   714      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   715      offset_of_heading_in_problem conjsN problem 0,
   716      fact_names |> Vector.fromList)
   717   end
   718 
   719 (* FUDGE *)
   720 val conj_weight = 0.0
   721 val hyp_weight = 0.1
   722 val fact_min_weight = 0.2
   723 val fact_max_weight = 1.0
   724 
   725 fun add_term_weights weight (ATerm (s, tms)) =
   726   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   727   #> fold (add_term_weights weight) tms
   728 fun add_problem_line_weights weight (Fof (_, _, phi, _)) =
   729   fold_formula (add_term_weights weight) phi
   730 
   731 fun add_conjectures_weights [] = I
   732   | add_conjectures_weights conjs =
   733     let val (hyps, conj) = split_last conjs in
   734       add_problem_line_weights conj_weight conj
   735       #> fold (add_problem_line_weights hyp_weight) hyps
   736     end
   737 
   738 fun add_facts_weights facts =
   739   let
   740     val num_facts = length facts
   741     fun weight_of j =
   742       fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
   743                         / Real.fromInt num_facts
   744   in
   745     map weight_of (0 upto num_facts - 1) ~~ facts
   746     |> fold (uncurry add_problem_line_weights)
   747   end
   748 
   749 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
   750 fun atp_problem_weights problem =
   751   Symtab.empty
   752   |> add_conjectures_weights (these (AList.lookup (op =) problem conjsN))
   753   |> add_facts_weights (these (AList.lookup (op =) problem factsN))
   754   |> Symtab.dest
   755   |> sort (prod_ord Real.compare string_ord o pairself swap)
   756 
   757 end;