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