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