src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
author blanchet
Sun May 01 18:37:25 2011 +0200 (2011-05-01)
changeset 42569 5737947e4c77
parent 42568 7b9801a34836
child 42570 77f94ac04f32
permissions -rw-r--r--
make sure that fequal keeps its type arguments for mangled type systems
     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     Many_Typed |
    17     Mangled of bool |
    18     Args of bool |
    19     Tags of bool |
    20     No_Types
    21 
    22   val readable_names : bool Unsynchronized.ref
    23   val fact_prefix : string
    24   val conjecture_prefix : string
    25   val predicator_base : string
    26   val explicit_app_base : string
    27   val type_pred_base : string
    28   val tff_type_prefix : string
    29   val is_type_system_sound : type_system -> bool
    30   val type_system_types_dangerous_types : type_system -> bool
    31   val num_atp_type_args : theory -> type_system -> string -> int
    32   val unmangled_const : string -> string * string fo_term list
    33   val translate_atp_fact :
    34     Proof.context -> bool -> (string * 'a) * thm
    35     -> translated_formula option * ((string * 'a) * thm)
    36   val prepare_atp_problem :
    37     Proof.context -> type_system -> bool -> term list -> term
    38     -> (translated_formula option * ((string * 'a) * thm)) list
    39     -> string problem * string Symtab.table * int * int
    40        * (string * 'a) list vector
    41   val atp_problem_weights : string problem -> (string * real) list
    42 end;
    43 
    44 structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
    45 struct
    46 
    47 open ATP_Problem
    48 open Metis_Translate
    49 open Sledgehammer_Util
    50 
    51 (* Readable names are often much shorter, especially if types are mangled in
    52    names. For that reason, they are on by default. *)
    53 val readable_names = Unsynchronized.ref true
    54 
    55 val type_decl_prefix = "type_"
    56 val sym_decl_prefix = "sym_"
    57 val fact_prefix = "fact_"
    58 val conjecture_prefix = "conj_"
    59 val helper_prefix = "help_"
    60 val class_rel_clause_prefix = "crel_";
    61 val arity_clause_prefix = "arity_"
    62 val tfree_prefix = "tfree_"
    63 
    64 val predicator_base = "hBOOL"
    65 val explicit_app_base = "hAPP"
    66 val type_pred_base = "is"
    67 val tff_type_prefix = "ty_"
    68 
    69 fun make_tff_type s = tff_type_prefix ^ ascii_of s
    70 
    71 (* official TPTP syntax *)
    72 val tptp_tff_type_of_types = "$tType"
    73 val tptp_tff_bool_type = "$o"
    74 val tptp_false = "$false"
    75 val tptp_true = "$true"
    76 
    77 (* Freshness almost guaranteed! *)
    78 val sledgehammer_weak_prefix = "Sledgehammer:"
    79 
    80 type translated_formula =
    81   {name: string,
    82    kind: formula_kind,
    83    combformula: (name, typ, combterm) formula,
    84    atomic_types: typ list}
    85 
    86 fun update_combformula f
    87         ({name, kind, combformula, atomic_types} : translated_formula) =
    88   {name = name, kind = kind, combformula = f combformula,
    89    atomic_types = atomic_types} : translated_formula
    90 
    91 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
    92 
    93 datatype type_system =
    94   Many_Typed |
    95   Mangled of bool |
    96   Args of bool |
    97   Tags of bool |
    98   No_Types
    99 
   100 fun is_type_system_sound Many_Typed = true
   101   | is_type_system_sound (Mangled full_types) = full_types
   102   | is_type_system_sound (Args full_types) = full_types
   103   | is_type_system_sound (Tags full_types) = full_types
   104   | is_type_system_sound No_Types = false
   105 
   106 fun type_system_types_dangerous_types (Tags _) = true
   107   | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys
   108 
   109 fun dont_need_type_args type_sys s =
   110   s <> type_pred_base andalso
   111   (member (op =) [@{const_name HOL.eq}] s orelse
   112    case type_sys of
   113      Many_Typed => false
   114    | Mangled _ => false
   115    | Args _ => s = explicit_app_base
   116    | Tags full_types => full_types orelse s = explicit_app_base
   117    | No_Types => true)
   118 
   119 datatype type_arg_policy = No_Type_Args | Mangled_Types | Explicit_Type_Args
   120 
   121 fun general_type_arg_policy Many_Typed = Mangled_Types
   122   | general_type_arg_policy (Mangled _) = Mangled_Types
   123   | general_type_arg_policy _ = Explicit_Type_Args
   124 
   125 fun type_arg_policy type_sys s =
   126   if dont_need_type_args type_sys s then No_Type_Args
   127   else general_type_arg_policy type_sys
   128 
   129 fun num_atp_type_args thy type_sys s =
   130   if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s
   131   else 0
   132 
   133 fun atp_type_literals_for_types type_sys kind Ts =
   134   if type_sys = No_Types then
   135     []
   136   else
   137     Ts |> type_literals_for_types
   138        |> filter (fn TyLitVar _ => kind <> Conjecture
   139                    | TyLitFree _ => kind = Conjecture)
   140 
   141 fun mk_anot phi = AConn (ANot, [phi])
   142 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
   143 fun mk_aconns c phis =
   144   let val (phis', phi') = split_last phis in
   145     fold_rev (mk_aconn c) phis' phi'
   146   end
   147 fun mk_ahorn [] phi = phi
   148   | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
   149 fun mk_aquant _ [] phi = phi
   150   | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
   151     if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
   152   | mk_aquant q xs phi = AQuant (q, xs, phi)
   153 
   154 fun close_universally atom_vars phi =
   155   let
   156     fun formula_vars bounds (AQuant (_, xs, phi)) =
   157         formula_vars (map fst xs @ bounds) phi
   158       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   159       | formula_vars bounds (AAtom tm) =
   160         union (op =) (atom_vars tm []
   161                       |> filter_out (member (op =) bounds o fst))
   162   in mk_aquant AForall (formula_vars [] phi []) phi end
   163 
   164 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
   165   | combterm_vars (CombConst _) = I
   166   | combterm_vars (CombVar (name, ty)) = insert (op =) (name, SOME ty)
   167 val close_combformula_universally = close_universally combterm_vars
   168 
   169 fun term_vars (ATerm (name as (s, _), tms)) =
   170   is_atp_variable s ? insert (op =) (name, NONE)
   171   #> fold term_vars tms
   172 val close_formula_universally = close_universally term_vars
   173 
   174 fun fo_term_from_typ (Type (s, Ts)) =
   175     ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts)
   176   | fo_term_from_typ (TFree (s, _)) =
   177     ATerm (`make_fixed_type_var s, [])
   178   | fo_term_from_typ (TVar ((x as (s, _)), _)) =
   179     ATerm ((make_schematic_type_var x, s), [])
   180 
   181 (* This shouldn't clash with anything else. *)
   182 val mangled_type_sep = "\000"
   183 
   184 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   185   | generic_mangled_type_name f (ATerm (name, tys)) =
   186     f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")"
   187 val mangled_type_name =
   188   fo_term_from_typ
   189   #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),
   190                 generic_mangled_type_name snd ty))
   191 
   192 fun generic_mangled_type_suffix f g tys =
   193   fold_rev (curry (op ^) o g o prefix mangled_type_sep
   194             o generic_mangled_type_name f) tys ""
   195 fun mangled_const_name T_args (s, s') =
   196   let val ty_args = map fo_term_from_typ T_args in
   197     (s ^ generic_mangled_type_suffix fst ascii_of ty_args,
   198      s' ^ generic_mangled_type_suffix snd I ty_args)
   199   end
   200 
   201 val parse_mangled_ident =
   202   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
   203 
   204 fun parse_mangled_type x =
   205   (parse_mangled_ident
   206    -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
   207                     [] >> ATerm) x
   208 and parse_mangled_types x =
   209   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
   210 
   211 fun unmangled_type s =
   212   s |> suffix ")" |> raw_explode
   213     |> Scan.finite Symbol.stopper
   214            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
   215                                                 quote s)) parse_mangled_type))
   216     |> fst
   217 
   218 val unmangled_const_name = space_explode mangled_type_sep #> hd
   219 fun unmangled_const s =
   220   let val ss = space_explode mangled_type_sep s in
   221     (hd ss, map unmangled_type (tl ss))
   222   end
   223 
   224 val introduce_proxies =
   225   let
   226     fun aux top_level (CombApp (tm1, tm2)) =
   227         CombApp (aux top_level tm1, aux false tm2)
   228       | aux top_level (CombConst (name as (s, s'), ty, ty_args)) =
   229         (case AList.lookup (op =) metis_proxies s of
   230            SOME proxy_base =>
   231            if top_level then
   232              (case s of
   233                 "c_False" => (tptp_false, s')
   234               | "c_True" => (tptp_true, s')
   235               | _ => name, [])
   236            else
   237              (proxy_base |>> prefix const_prefix, ty_args)
   238           | NONE => (name, ty_args))
   239         |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
   240       | aux _ tm = tm
   241   in aux true end
   242 
   243 fun combformula_from_prop thy eq_as_iff =
   244   let
   245     fun do_term bs t atomic_types =
   246       combterm_from_term thy bs (Envir.eta_contract t)
   247       |>> (introduce_proxies #> AAtom)
   248       ||> union (op =) atomic_types
   249     fun do_quant bs q s T t' =
   250       let val s = Name.variant (map fst bs) s in
   251         do_formula ((s, T) :: bs) t'
   252         #>> mk_aquant q [(`make_bound_var s, SOME T)]
   253       end
   254     and do_conn bs c t1 t2 =
   255       do_formula bs t1 ##>> do_formula bs t2
   256       #>> uncurry (mk_aconn c)
   257     and do_formula bs t =
   258       case t of
   259         @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
   260       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   261         do_quant bs AForall s T t'
   262       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   263         do_quant bs AExists s T t'
   264       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
   265       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
   266       | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
   267       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   268         if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
   269       | _ => do_term bs t
   270   in do_formula [] end
   271 
   272 val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
   273 
   274 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
   275 fun conceal_bounds Ts t =
   276   subst_bounds (map (Free o apfst concealed_bound_name)
   277                     (0 upto length Ts - 1 ~~ Ts), t)
   278 fun reveal_bounds Ts =
   279   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   280                     (0 upto length Ts - 1 ~~ Ts))
   281 
   282 (* Removes the lambdas from an equation of the form "t = (%x. u)".
   283    (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
   284 fun extensionalize_term t =
   285   let
   286     fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
   287       | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
   288                                         Type (_, [_, res_T])]))
   289                     $ t2 $ Abs (var_s, var_T, t')) =
   290         if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
   291           let val var_t = Var ((var_s, j), var_T) in
   292             Const (s, T' --> T' --> res_T)
   293               $ betapply (t2, var_t) $ subst_bound (var_t, t')
   294             |> aux (j + 1)
   295           end
   296         else
   297           t
   298       | aux _ t = t
   299   in aux (maxidx_of_term t + 1) t end
   300 
   301 fun introduce_combinators_in_term ctxt kind t =
   302   let val thy = Proof_Context.theory_of ctxt in
   303     if Meson.is_fol_term thy t then
   304       t
   305     else
   306       let
   307         fun aux Ts t =
   308           case t of
   309             @{const Not} $ t1 => @{const Not} $ aux Ts t1
   310           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   311             t0 $ Abs (s, T, aux (T :: Ts) t')
   312           | (t0 as Const (@{const_name All}, _)) $ t1 =>
   313             aux Ts (t0 $ eta_expand Ts t1 1)
   314           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   315             t0 $ Abs (s, T, aux (T :: Ts) t')
   316           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   317             aux Ts (t0 $ eta_expand Ts t1 1)
   318           | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   319           | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   320           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   321           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   322               $ t1 $ t2 =>
   323             t0 $ aux Ts t1 $ aux Ts t2
   324           | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   325                    t
   326                  else
   327                    t |> conceal_bounds Ts
   328                      |> Envir.eta_contract
   329                      |> cterm_of thy
   330                      |> Meson_Clausify.introduce_combinators_in_cterm
   331                      |> prop_of |> Logic.dest_equals |> snd
   332                      |> reveal_bounds Ts
   333         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   334       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   335       handle THM _ =>
   336              (* A type variable of sort "{}" will make abstraction fail. *)
   337              if kind = Conjecture then HOLogic.false_const
   338              else HOLogic.true_const
   339   end
   340 
   341 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   342    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
   343 fun freeze_term t =
   344   let
   345     fun aux (t $ u) = aux t $ aux u
   346       | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   347       | aux (Var ((s, i), T)) =
   348         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   349       | aux t = t
   350   in t |> exists_subterm is_Var t ? aux end
   351 
   352 (* making fact and conjecture formulas *)
   353 fun make_formula ctxt eq_as_iff presimp name kind t =
   354   let
   355     val thy = Proof_Context.theory_of ctxt
   356     val t = t |> Envir.beta_eta_contract
   357               |> transform_elim_term
   358               |> Object_Logic.atomize_term thy
   359     val need_trueprop = (fastype_of t = @{typ bool})
   360     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   361               |> extensionalize_term
   362               |> presimp ? presimplify_term thy
   363               |> perhaps (try (HOLogic.dest_Trueprop))
   364               |> introduce_combinators_in_term ctxt kind
   365               |> kind <> Axiom ? freeze_term
   366     val (combformula, atomic_types) =
   367       combformula_from_prop thy eq_as_iff t []
   368   in
   369     {name = name, combformula = combformula, kind = kind,
   370      atomic_types = atomic_types}
   371   end
   372 
   373 fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), t) =
   374   case (keep_trivial, make_formula ctxt eq_as_iff presimp name Axiom t) of
   375     (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
   376     NONE
   377   | (_, formula) => SOME formula
   378 
   379 fun make_conjecture ctxt ts =
   380   let val last = length ts - 1 in
   381     map2 (fn j => make_formula ctxt true true (string_of_int j)
   382                                (if j = last then Conjecture else Hypothesis))
   383          (0 upto last) ts
   384   end
   385 
   386 (** Helper facts **)
   387 
   388 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
   389   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
   390   | formula_map f (AAtom tm) = AAtom (f tm)
   391 
   392 fun formula_fold f (AQuant (_, _, phi)) = formula_fold f phi
   393   | formula_fold f (AConn (_, phis)) = fold (formula_fold f) phis
   394   | formula_fold f (AAtom tm) = f tm
   395 
   396 type sym_table_info =
   397   {pred_sym : bool, min_ary : int, max_ary : int, typ : typ option}
   398 
   399 fun ti_ti_helper_fact () =
   400   let
   401     fun var s = ATerm (`I s, [])
   402     fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
   403   in
   404     Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom,
   405              AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
   406              |> close_formula_universally, NONE, NONE)
   407   end
   408 
   409 fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_table_info) =
   410   case strip_prefix_and_unascii const_prefix s of
   411     SOME mangled_s =>
   412     let
   413       val thy = Proof_Context.theory_of ctxt
   414       val unmangled_s = mangled_s |> unmangled_const_name
   415       fun dub_and_inst c needs_full_types (th, j) =
   416         ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""),
   417           false),
   418          let val t = th |> prop_of in
   419            t |> (general_type_arg_policy type_sys = Mangled_Types andalso
   420                  not (null (Term.hidden_polymorphism t)))
   421                 ? (case typ of
   422                      SOME T =>
   423                      specialize_type thy (safe_invert_const unmangled_s, T)
   424                    | NONE => I)
   425          end)
   426       fun make_facts eq_as_iff =
   427         map_filter (make_fact ctxt false eq_as_iff false)
   428     in
   429       metis_helpers
   430       |> maps (fn (metis_s, (needs_full_types, ths)) =>
   431                   if metis_s <> unmangled_s orelse
   432                      (needs_full_types andalso
   433                       not (type_system_types_dangerous_types type_sys)) then
   434                     []
   435                   else
   436                     ths ~~ (1 upto length ths)
   437                     |> map (dub_and_inst mangled_s needs_full_types)
   438                     |> make_facts (not needs_full_types))
   439     end
   440   | NONE => []
   441 fun helper_facts_for_sym_table ctxt type_sys sym_tab =
   442   Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab []
   443 
   444 fun translate_atp_fact ctxt keep_trivial =
   445   `(make_fact ctxt keep_trivial true true o apsnd prop_of)
   446 
   447 fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
   448   let
   449     val thy = Proof_Context.theory_of ctxt
   450     val fact_ts = map (prop_of o snd o snd) rich_facts
   451     val (facts, fact_names) =
   452       rich_facts
   453       |> map_filter (fn (NONE, _) => NONE
   454                       | (SOME fact, (name, _)) => SOME (fact, name))
   455       |> ListPair.unzip
   456     (* Remove existing facts from the conjecture, as this can dramatically
   457        boost an ATP's performance (for some reason). *)
   458     val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
   459     val goal_t = Logic.list_implies (hyp_ts, concl_t)
   460     val all_ts = goal_t :: fact_ts
   461     val subs = tfree_classes_of_terms all_ts
   462     val supers = tvar_classes_of_terms all_ts
   463     val tycons = type_consts_of_terms thy all_ts
   464     val conjs = make_conjecture ctxt (hyp_ts @ [concl_t])
   465     val (supers', arity_clauses) =
   466       if type_sys = No_Types then ([], [])
   467       else make_arity_clauses thy tycons supers
   468     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   469   in
   470     (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
   471   end
   472 
   473 fun impose_type_arg_policy type_sys =
   474   let
   475     fun aux (CombApp tmp) = CombApp (pairself aux tmp)
   476       | aux (CombConst (name as (s, _), ty, ty_args)) =
   477         (case strip_prefix_and_unascii const_prefix s of
   478            NONE => (name, ty_args)
   479          | SOME s'' =>
   480            let val s'' = safe_invert_const s'' in
   481              case type_arg_policy type_sys s'' of
   482                No_Type_Args => (name, [])
   483              | Mangled_Types => (mangled_const_name ty_args name, [])
   484              | Explicit_Type_Args => (name, ty_args)
   485            end)
   486         |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
   487       | aux tm = tm
   488   in aux end
   489 val impose_type_arg_policy_on_fact =
   490   update_combformula o formula_map o impose_type_arg_policy
   491 
   492 fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t])
   493 
   494 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
   495     (true, ATerm (class, [ATerm (name, [])]))
   496   | fo_literal_from_type_literal (TyLitFree (class, name)) =
   497     (true, ATerm (class, [ATerm (name, [])]))
   498 
   499 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   500 
   501 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
   502    considered dangerous because their "exhaust" properties can easily lead to
   503    unsound ATP proofs. The checks below are an (unsound) approximation of
   504    finiteness. *)
   505 
   506 fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true
   507   | is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) =
   508     is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us
   509   | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false
   510 and is_type_dangerous ctxt (Type (s, Ts)) =
   511     is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts
   512   | is_type_dangerous _ _ = false
   513 and is_type_constr_dangerous ctxt s =
   514   let val thy = Proof_Context.theory_of ctxt in
   515     case Datatype_Data.get_info thy s of
   516       SOME {descr, ...} =>
   517       forall (fn (_, (_, _, constrs)) =>
   518                  forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr
   519     | NONE =>
   520       case Typedef.get_info ctxt s of
   521         ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type
   522       | [] => true
   523   end
   524 
   525 fun should_tag_with_type ctxt (Tags full_types) T =
   526     full_types orelse is_type_dangerous ctxt T
   527   | should_tag_with_type _ _ _ = false
   528 
   529 fun type_pred_combatom type_sys T tm =
   530   CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
   531            tm)
   532   |> impose_type_arg_policy type_sys
   533   |> AAtom
   534 
   535 fun formula_from_combformula ctxt type_sys =
   536   let
   537     fun do_term top_level u =
   538       let
   539         val (head, args) = strip_combterm_comb u
   540         val (x, ty_args) =
   541           case head of
   542             CombConst (name, _, ty_args) => (name, ty_args)
   543           | CombVar (name, _) => (name, [])
   544           | CombApp _ => raise Fail "impossible \"CombApp\""
   545         val t = ATerm (x, map fo_term_from_typ ty_args @
   546                           map (do_term false) args)
   547         val ty = combtyp_of u
   548       in
   549         t |> (if not top_level andalso
   550                  should_tag_with_type ctxt type_sys ty then
   551                 tag_with_type (fo_term_from_typ ty)
   552               else
   553                 I)
   554       end
   555     val do_bound_type =
   556       if type_sys = Many_Typed then SOME o mangled_type_name else K NONE
   557     val do_out_of_bound_type =
   558       if member (op =) [Mangled true, Args true] type_sys then
   559         (fn (s, ty) =>
   560             type_pred_combatom type_sys ty (CombVar (s, ty))
   561             |> formula_from_combformula ctxt type_sys |> SOME)
   562       else
   563         K NONE
   564     fun do_formula (AQuant (q, xs, phi)) =
   565         AQuant (q, xs |> map (apsnd (fn NONE => NONE
   566                                       | SOME ty => do_bound_type ty)),
   567                 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
   568                     (map_filter
   569                          (fn (_, NONE) => NONE
   570                            | (s, SOME ty) => do_out_of_bound_type (s, ty)) xs)
   571                     (do_formula phi))
   572       | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
   573       | do_formula (AAtom tm) = AAtom (do_term true tm)
   574   in do_formula end
   575 
   576 fun formula_for_fact ctxt type_sys
   577                      ({combformula, atomic_types, ...} : translated_formula) =
   578   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
   579                 (atp_type_literals_for_types type_sys Axiom atomic_types))
   580            (formula_from_combformula ctxt type_sys
   581                 (close_combformula_universally combformula))
   582   |> close_formula_universally
   583 
   584 fun logic_for_type_sys Many_Typed = Tff
   585   | logic_for_type_sys _ = Fof
   586 
   587 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   588    of monomorphization). The TPTP explicitly forbids name clashes, and some of
   589    the remote provers might care. *)
   590 fun formula_line_for_fact ctxt prefix type_sys
   591                           (j, formula as {name, kind, ...}) =
   592   Formula (logic_for_type_sys type_sys,
   593            prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
   594            formula_for_fact ctxt type_sys formula, NONE, NONE)
   595 
   596 fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
   597                                                        superclass, ...}) =
   598   let val ty_arg = ATerm (`I "T", []) in
   599     Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom,
   600              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   601                                AAtom (ATerm (superclass, [ty_arg]))])
   602              |> close_formula_universally, NONE, NONE)
   603   end
   604 
   605 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
   606     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   607   | fo_literal_from_arity_literal (TVarLit (c, sort)) =
   608     (false, ATerm (c, [ATerm (sort, [])]))
   609 
   610 fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   611                                                 ...}) =
   612   Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom,
   613            mk_ahorn (map (formula_from_fo_literal o apfst not
   614                           o fo_literal_from_arity_literal) premLits)
   615                     (formula_from_fo_literal
   616                          (fo_literal_from_arity_literal conclLit))
   617            |> close_formula_universally, NONE, NONE)
   618 
   619 fun formula_line_for_conjecture ctxt type_sys
   620         ({name, kind, combformula, ...} : translated_formula) =
   621   Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind,
   622            formula_from_combformula ctxt type_sys
   623                                     (close_combformula_universally combformula)
   624            |> close_formula_universally, NONE, NONE)
   625 
   626 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
   627   atomic_types |> atp_type_literals_for_types type_sys Conjecture
   628                |> map fo_literal_from_type_literal
   629 
   630 fun formula_line_for_free_type j lit =
   631   Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis,
   632            formula_from_fo_literal lit, NONE, NONE)
   633 fun formula_lines_for_free_types type_sys facts =
   634   let
   635     val litss = map (free_type_literals type_sys) facts
   636     val lits = fold (union (op =)) litss []
   637   in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
   638 
   639 (** "hBOOL" and "hAPP" **)
   640 
   641 fun add_combterm_to_sym_table explicit_apply =
   642   let
   643     fun aux top_level tm =
   644       let val (head, args) = strip_combterm_comb tm in
   645         (case head of
   646            CombConst ((s, _), T, _) =>
   647            if String.isPrefix bound_var_prefix s then
   648              I
   649            else
   650              let val ary = length args in
   651                Symtab.map_default
   652                    (s, {pred_sym = true,
   653                         min_ary = if explicit_apply then 0 else ary,
   654                         max_ary = 0, typ = SOME T})
   655                    (fn {pred_sym, min_ary, max_ary, typ} =>
   656                        {pred_sym = pred_sym andalso top_level,
   657                         min_ary = Int.min (ary, min_ary),
   658                         max_ary = Int.max (ary, max_ary),
   659                         typ = if typ = SOME T then typ else NONE})
   660             end
   661          | _ => I)
   662         #> fold (aux false) args
   663       end
   664   in aux true end
   665 
   666 val add_fact_to_sym_table = fact_lift o formula_fold o add_combterm_to_sym_table
   667 
   668 val default_sym_table_entries =
   669   [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
   670    (make_fixed_const predicator_base,
   671     {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
   672   ([tptp_false, tptp_true]
   673    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
   674 
   675 fun sym_table_for_facts explicit_apply facts =
   676   Symtab.empty |> fold Symtab.default default_sym_table_entries
   677                |> fold (add_fact_to_sym_table explicit_apply) facts
   678 
   679 fun min_arity_of sym_tab s =
   680   case Symtab.lookup sym_tab s of
   681     SOME ({min_ary, ...} : sym_table_info) => min_ary
   682   | NONE =>
   683     case strip_prefix_and_unascii const_prefix s of
   684       SOME s =>
   685       let val s = s |> unmangled_const_name |> safe_invert_const in
   686         if s = predicator_base then 1
   687         else if s = explicit_app_base then 2
   688         else if s = type_pred_base then 1
   689         else 0
   690       end
   691     | NONE => 0
   692 
   693 (* True if the constant ever appears outside of the top-level position in
   694    literals, or if it appears with different arities (e.g., because of different
   695    type instantiations). If false, the constant always receives all of its
   696    arguments and is used as a predicate. *)
   697 fun is_pred_sym sym_tab s =
   698   case Symtab.lookup sym_tab s of
   699     SOME {pred_sym, min_ary, max_ary, ...} => pred_sym andalso min_ary = max_ary
   700   | NONE => false
   701 
   702 val predicator_combconst =
   703   CombConst (`make_fixed_const predicator_base, @{typ "bool => bool"}, [])
   704 fun predicator tm = CombApp (predicator_combconst, tm)
   705 
   706 fun introduce_predicators_in_combterm sym_tab tm =
   707   case strip_combterm_comb tm of
   708     (CombConst ((s, _), _, _), _) =>
   709     if is_pred_sym sym_tab s then tm else predicator tm
   710   | _ => predicator tm
   711 
   712 fun list_app head args = fold (curry (CombApp o swap)) args head
   713 
   714 fun explicit_app arg head =
   715   let
   716     val head_T = combtyp_of head
   717     val (arg_T, res_T) = dest_funT head_T
   718     val explicit_app =
   719       CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
   720                  [arg_T, res_T])
   721   in list_app explicit_app [head, arg] end
   722 fun list_explicit_app head args = fold explicit_app args head
   723 
   724 fun introduce_explicit_apps_in_combterm sym_tab =
   725   let
   726     fun aux tm =
   727       case strip_combterm_comb tm of
   728         (head as CombConst ((s, _), _, _), args) =>
   729         args |> map aux
   730              |> chop (min_arity_of sym_tab s)
   731              |>> list_app head
   732              |-> list_explicit_app
   733       | (head, args) => list_explicit_app head (map aux args)
   734   in aux end
   735 
   736 fun firstorderize_combterm sym_tab =
   737   introduce_explicit_apps_in_combterm sym_tab
   738   #> introduce_predicators_in_combterm sym_tab
   739 val firstorderize_fact =
   740   update_combformula o formula_map o firstorderize_combterm
   741 
   742 fun is_const_relevant type_sys sym_tab s =
   743   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   744   (type_sys = Many_Typed orelse not (is_pred_sym sym_tab s))
   745 
   746 fun consider_combterm_consts type_sys sym_tab tm =
   747   let val (head, args) = strip_combterm_comb tm in
   748     (case head of
   749        CombConst ((s, s'), ty, ty_args) =>
   750        (* FIXME: exploit type subsumption *)
   751        is_const_relevant type_sys sym_tab s
   752        ? Symtab.insert_list (op =) (s, (s', ty_args, ty))
   753      | _ => I)
   754     #> fold (consider_combterm_consts type_sys sym_tab) args
   755   end
   756 
   757 fun consider_fact_consts type_sys sym_tab =
   758   fact_lift (formula_fold (consider_combterm_consts type_sys sym_tab))
   759 
   760 (* FIXME: needed? *)
   761 fun typed_const_table_for_facts type_sys sym_tab facts =
   762   Symtab.empty |> member (op =) [Many_Typed, Mangled true, Args true] type_sys
   763                   ? fold (consider_fact_consts type_sys sym_tab) facts
   764 
   765 fun strip_and_map_type 0 f T = ([], f T)
   766   | strip_and_map_type n f (Type (@{type_name fun}, [dom_T, ran_T])) =
   767     strip_and_map_type (n - 1) f ran_T |>> cons (f dom_T)
   768   | strip_and_map_type _ _ _ = raise Fail "unexpected non-function"
   769 
   770 fun problem_line_for_typed_const ctxt type_sys sym_tab s n j (s', ty_args, T) =
   771   let val ary = min_arity_of sym_tab s in
   772     if type_sys = Many_Typed then
   773       let val (arg_Ts, res_T) = strip_and_map_type ary mangled_type_name T in
   774         Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_Ts,
   775               (* ### FIXME: put that in typed_const_tab *)
   776               if is_pred_sym sym_tab s then `I tptp_tff_bool_type else res_T)
   777       end
   778     else
   779       let
   780         val (arg_Ts, res_T) = strip_and_map_type ary I T
   781         val bound_names =
   782           1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
   783         val bound_tms =
   784           bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
   785         val bound_Ts = arg_Ts |> map (if n > 1 then SOME else K NONE)
   786         val freshener =
   787           case type_sys of Args _ => string_of_int j ^ "_" | _ => ""
   788       in
   789         Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom,
   790                  CombConst ((s, s'), T, ty_args)
   791                  |> fold (curry (CombApp o swap)) bound_tms
   792                  |> type_pred_combatom type_sys res_T
   793                  |> mk_aquant AForall (bound_names ~~ bound_Ts)
   794                  |> formula_from_combformula ctxt type_sys,
   795                  NONE, NONE)
   796       end
   797   end
   798 fun problem_lines_for_sym_decl ctxt type_sys sym_tab (s, xs) =
   799   let val n = length xs in
   800     map2 (problem_line_for_typed_const ctxt type_sys sym_tab s n)
   801          (0 upto n - 1) xs
   802   end
   803 fun problem_lines_for_sym_decls ctxt type_sys sym_tab typed_const_tab =
   804   Symtab.fold_rev (append o problem_lines_for_sym_decl ctxt type_sys sym_tab)
   805                   typed_const_tab []
   806 
   807 fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
   808     union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
   809   | add_tff_types_in_formula (AConn (_, phis)) =
   810     fold add_tff_types_in_formula phis
   811   | add_tff_types_in_formula (AAtom _) = I
   812 
   813 fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
   814     union (op =) (res_T :: arg_Ts)
   815   | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) =
   816     add_tff_types_in_formula phi
   817 
   818 fun tff_types_in_problem problem =
   819   fold (fold add_tff_types_in_problem_line o snd) problem []
   820 
   821 fun decl_line_for_tff_type (s, s') =
   822   Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_tff_type_of_types)
   823 
   824 val type_declsN = "Types"
   825 val sym_declsN = "Symbol types"
   826 val factsN = "Relevant facts"
   827 val class_relsN = "Class relationships"
   828 val aritiesN = "Arities"
   829 val helpersN = "Helper facts"
   830 val conjsN = "Conjectures"
   831 val free_typesN = "Type variables"
   832 
   833 fun offset_of_heading_in_problem _ [] j = j
   834   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
   835     if heading = needle then j
   836     else offset_of_heading_in_problem needle problem (j + length lines)
   837 
   838 fun prepare_atp_problem ctxt type_sys explicit_apply hyp_ts concl_t facts =
   839   let
   840     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
   841       translate_formulas ctxt type_sys hyp_ts concl_t facts
   842     val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
   843     val (conjs, facts) =
   844       (conjs, facts) |> pairself (map (firstorderize_fact sym_tab))
   845     val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
   846     val (conjs, facts) =
   847       (conjs, facts) |> pairself (map (impose_type_arg_policy_on_fact type_sys))
   848     val sym_tab' = conjs @ facts |> sym_table_for_facts false
   849     val typed_const_tab =
   850       conjs @ facts |> typed_const_table_for_facts type_sys sym_tab'
   851     val sym_decl_lines =
   852       typed_const_tab |> problem_lines_for_sym_decls ctxt type_sys sym_tab'
   853     val helpers = helper_facts_for_sym_table ctxt type_sys sym_tab'
   854                   |> map (firstorderize_fact sym_tab
   855                           #> impose_type_arg_policy_on_fact type_sys)
   856     (* Reordering these might confuse the proof reconstruction code or the SPASS
   857        Flotter hack. *)
   858     val problem =
   859       [(sym_declsN, sym_decl_lines),
   860        (factsN, map (formula_line_for_fact ctxt fact_prefix type_sys)
   861                     (0 upto length facts - 1 ~~ facts)),
   862        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
   863        (aritiesN, map formula_line_for_arity_clause arity_clauses),
   864        (helpersN, map (formula_line_for_fact ctxt helper_prefix type_sys)
   865                       (0 upto length helpers - 1 ~~ helpers)
   866                   |> (if type_sys = Tags false then cons (ti_ti_helper_fact ())
   867                       else I)),
   868        (conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs),
   869        (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
   870     val problem =
   871       problem
   872       |> (if type_sys = Many_Typed then
   873             cons (type_declsN,
   874                   map decl_line_for_tff_type (tff_types_in_problem problem))
   875           else
   876             I)
   877     val (problem, pool) = problem |> nice_atp_problem (!readable_names)
   878   in
   879     (problem,
   880      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   881      offset_of_heading_in_problem factsN problem 0,
   882      offset_of_heading_in_problem conjsN problem 0,
   883      fact_names |> Vector.fromList)
   884   end
   885 
   886 (* FUDGE *)
   887 val conj_weight = 0.0
   888 val hyp_weight = 0.1
   889 val fact_min_weight = 0.2
   890 val fact_max_weight = 1.0
   891 
   892 fun add_term_weights weight (ATerm (s, tms)) =
   893   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   894   #> fold (add_term_weights weight) tms
   895 fun add_problem_line_weights weight (Formula (_, _, _, phi, _, _)) =
   896     formula_fold (add_term_weights weight) phi
   897   | add_problem_line_weights _ _ = I
   898 
   899 fun add_conjectures_weights [] = I
   900   | add_conjectures_weights conjs =
   901     let val (hyps, conj) = split_last conjs in
   902       add_problem_line_weights conj_weight conj
   903       #> fold (add_problem_line_weights hyp_weight) hyps
   904     end
   905 
   906 fun add_facts_weights facts =
   907   let
   908     val num_facts = length facts
   909     fun weight_of j =
   910       fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
   911                         / Real.fromInt num_facts
   912   in
   913     map weight_of (0 upto num_facts - 1) ~~ facts
   914     |> fold (uncurry add_problem_line_weights)
   915   end
   916 
   917 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
   918 fun atp_problem_weights problem =
   919   Symtab.empty
   920   |> add_conjectures_weights (these (AList.lookup (op =) problem conjsN))
   921   |> add_facts_weights (these (AList.lookup (op =) problem factsN))
   922   |> Symtab.dest
   923   |> sort (prod_ord Real.compare string_ord o pairself swap)
   924 
   925 end;