wneuper/isa: src/HOL/Tools/Sledgehammer/sledgehammer_atp

     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML

     2     Author:     Fabian Immler, TU Muenchen

     3     Author:     Makarius

     4     Author:     Jasmin Blanchette, TU Muenchen

     6 Translation of HOL to FOL for Sledgehammer.

     7 *)

     9 signature SLEDGEHAMMER_ATP_TRANSLATE =

    10 sig

    11   type 'a fo_term = 'a ATP_Problem.fo_term

    12   type format = ATP_Problem.format

    13   type formula_kind = ATP_Problem.formula_kind

    14   type 'a problem = 'a ATP_Problem.problem

    15   type locality = Sledgehammer_Filter.locality

    17   datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic

    18   datatype type_level =

    19     All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types

    20   datatype type_heaviness = Heavy | Light

    22   datatype type_system =

    23     Simple_Types of type_level |

    24     Preds of polymorphism * type_level * type_heaviness |

    25     Tags of polymorphism * type_level * type_heaviness

    27   type translated_formula

    29   val readable_names : bool Config.T

    30   val fact_prefix : string

    31   val conjecture_prefix : string

    32   val helper_prefix : string

    33   val typed_helper_suffix : string

    34   val predicator_name : string

    35   val app_op_name : string

    36   val type_pred_name : string

    37   val simple_type_prefix : string

    38   val type_sys_from_string : string -> type_system

    39   val polymorphism_of_type_sys : type_system -> polymorphism

    40   val level_of_type_sys : type_system -> type_level

    41   val is_type_sys_virtually_sound : type_system -> bool

    42   val is_type_sys_fairly_sound : type_system -> bool

    43   val unmangled_const : string -> string * string fo_term list

    44   val translate_atp_fact :

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

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

    47   val prepare_atp_problem :

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

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

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

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

    52        * (string * 'a) list vector * int list * int Symtab.table

    53   val atp_problem_weights : string problem -> (string * real) list

    54 end;

    56 structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =

    57 struct

    59 open ATP_Problem

    60 open Metis_Translate

    61 open Sledgehammer_Util

    62 open Sledgehammer_Filter

    64 (* experimental *)

    65 val generate_useful_info = false

    67 fun useful_isabelle_info s =

    68   if generate_useful_info then

    69     SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))

    70   else

    71     NONE

    73 val intro_info = useful_isabelle_info "intro"

    74 val elim_info = useful_isabelle_info "elim"

    75 val simp_info = useful_isabelle_info "simp"

    77 (* Readable names are often much shorter, especially if types are mangled in

    78    names. Also, the logic for generating legal SNARK sort names is only

    79    implemented for readable names. Finally, readable names are, well, more

    80    readable. For these reason, they are enabled by default. *)

    81 val readable_names =

    82   Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)

    84 val type_decl_prefix = "ty_"

    85 val sym_decl_prefix = "sy_"

    86 val sym_formula_prefix = "sym_"

    87 val fact_prefix = "fact_"

    88 val conjecture_prefix = "conj_"

    89 val helper_prefix = "help_"

    90 val class_rel_clause_prefix = "crel_";

    91 val arity_clause_prefix = "arity_"

    92 val tfree_prefix = "tfree_"

    94 val typed_helper_suffix = "_T"

    95 val untyped_helper_suffix = "_U"

    97 val predicator_name = "hBOOL"

    98 val app_op_name = "hAPP"

    99 val type_pred_name = "is"

   100 val simple_type_prefix = "ty_"

   102 fun make_simple_type s =

   103   if s = tptp_bool_type orelse s = tptp_fun_type orelse

   104      s = tptp_individual_type then

   105     s

   106   else

   107     simple_type_prefix ^ ascii_of s

   109 (* Freshness almost guaranteed! *)

   110 val sledgehammer_weak_prefix = "Sledgehammer:"

   112 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic

   113 datatype type_level =

   114   All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types

   115 datatype type_heaviness = Heavy | Light

   117 datatype type_system =

   118   Simple_Types of type_level |

   119   Preds of polymorphism * type_level * type_heaviness |

   120   Tags of polymorphism * type_level * type_heaviness

   122 fun try_unsuffixes ss s =

   123   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE

   125 fun type_sys_from_string s =

   126   (case try (unprefix "poly_") s of

   127      SOME s => (SOME Polymorphic, s)

   128    | NONE =>

   129      case try (unprefix "mono_") s of

   130        SOME s => (SOME Monomorphic, s)

   131      | NONE =>

   132        case try (unprefix "mangled_") s of

   133          SOME s => (SOME Mangled_Monomorphic, s)

   134        | NONE => (NONE, s))

   135   ||> (fn s =>

   136           (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)

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

   138             SOME s => (Nonmonotonic_Types, s)

   139           | NONE =>

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

   141               SOME s => (Finite_Types, s)

   142             | NONE => (All_Types, s))

   143   ||> apsnd (fn s =>

   144                 case try (unsuffix "_heavy") s of

   145                   SOME s => (Heavy, s)

   146                 | NONE => (Light, s))

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

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

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

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

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

   152            Tags (Polymorphic, All_Types, heaviness)

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

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

   155            Tags (Polymorphic, level, Heavy)

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

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

   158            Preds (poly, Const_Arg_Types, Light)

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

   160            Preds (Polymorphic, No_Types, Light)

   161          | _ => raise Same.SAME)

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

   164 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic

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

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

   168 fun level_of_type_sys (Simple_Types level) = level

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

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

   172 fun heaviness_of_type_sys (Simple_Types _) = Heavy

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

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

   176 fun is_type_level_virtually_sound level =

   177   level = All_Types orelse level = Nonmonotonic_Types

   178 val is_type_sys_virtually_sound =

   179   is_type_level_virtually_sound o level_of_type_sys

   181 fun is_type_level_fairly_sound level =

   182   is_type_level_virtually_sound level orelse level = Finite_Types

   183 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys

   185 fun is_setting_higher_order THF (Simple_Types _) = true

   186   | is_setting_higher_order _ _ = false

   188 type translated_formula =

   189   {name: string,

   190    locality: locality,

   191    kind: formula_kind,

   192    combformula: (name, typ, combterm) formula,

   193    atomic_types: typ list}

   195 fun update_combformula f ({name, locality, kind, combformula, atomic_types}

   196                           : translated_formula) =

   197   {name = name, locality = locality, kind = kind, combformula = f combformula,

   198    atomic_types = atomic_types} : translated_formula

   200 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula

   202 val type_instance = Sign.typ_instance o Proof_Context.theory_of

   204 fun insert_type ctxt get_T x xs =

   205   let val T = get_T x in

   206     if exists (curry (type_instance ctxt) T o get_T) xs then xs

   207     else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs

   208   end

   210 (* The Booleans indicate whether all type arguments should be kept. *)

   211 datatype type_arg_policy =

   212   Explicit_Type_Args of bool |

   213   Mangled_Type_Args of bool |

   214   No_Type_Args

   216 fun should_drop_arg_type_args (Simple_Types _) =

   217     false (* since TFF doesn't support overloading *)

   218   | should_drop_arg_type_args type_sys =

   219     level_of_type_sys type_sys = All_Types andalso

   220     heaviness_of_type_sys type_sys = Heavy

   222 fun general_type_arg_policy type_sys =

   223   if level_of_type_sys type_sys = No_Types then

   224     No_Type_Args

   225   else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then

   226     Mangled_Type_Args (should_drop_arg_type_args type_sys)

   227   else

   228     Explicit_Type_Args (should_drop_arg_type_args type_sys)

   230 fun type_arg_policy type_sys s =

   231   if s = @{const_name HOL.eq} orelse

   232      (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then

   233     No_Type_Args

   234   else

   235     general_type_arg_policy type_sys

   237 fun atp_type_literals_for_types format type_sys kind Ts =

   238   if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then

   239     []

   240   else

   241     Ts |> type_literals_for_types

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

   243                    | TyLitFree _ => kind = Conjecture)

   245 fun mk_aconns c phis =

   246   let val (phis', phi') = split_last phis in

   247     fold_rev (mk_aconn c) phis' phi'

   248   end

   249 fun mk_ahorn [] phi = phi

   250   | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])

   251 fun mk_aquant _ [] phi = phi

   252   | mk_aquant q xs (phi as AQuant (q', xs', phi')) =

   253     if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)

   254   | mk_aquant q xs phi = AQuant (q, xs, phi)

   256 fun close_universally atom_vars phi =

   257   let

   258     fun formula_vars bounds (AQuant (_, xs, phi)) =

   259         formula_vars (map fst xs @ bounds) phi

   260       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis

   261       | formula_vars bounds (AAtom tm) =

   262         union (op =) (atom_vars tm []

   263                       |> filter_out (member (op =) bounds o fst))

   264   in mk_aquant AForall (formula_vars [] phi []) phi end

   266 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]

   267   | combterm_vars (CombConst _) = I

   268   | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)

   269 fun close_combformula_universally phi = close_universally combterm_vars phi

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

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

   273 fun close_formula_universally phi = close_universally term_vars phi

   275 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)

   276 val homo_infinite_type = Type (homo_infinite_type_name, [])

   278 fun fo_term_from_typ higher_order =

   279   let

   280     fun term (Type (s, Ts)) =

   281       ATerm (case (higher_order, s) of

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

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

   284              | _ => if s = homo_infinite_type_name then `I tptp_individual_type

   285                     else `make_fixed_type_const s,

   286              map term Ts)

   287     | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])

   288     | term (TVar ((x as (s, _)), _)) =

   289       ATerm ((make_schematic_type_var x, s), [])

   290   in term end

   292 (* This shouldn't clash with anything else. *)

   293 val mangled_type_sep = "\000"

   295 fun generic_mangled_type_name f (ATerm (name, [])) = f name

   296   | generic_mangled_type_name f (ATerm (name, tys)) =

   297     f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)

   298     ^ ")"

   300 val bool_atype = AType (`I tptp_bool_type)

   302 fun ho_type_from_fo_term higher_order pred_sym ary =

   303   let

   304     fun to_atype ty =

   305       AType ((make_simple_type (generic_mangled_type_name fst ty),

   306               generic_mangled_type_name snd ty))

   307     fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))

   308     fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty

   309       | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys

   310     fun to_ho (ty as ATerm ((s, _), tys)) =

   311       if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty

   312   in if higher_order then to_ho else to_fo ary end

   314 fun mangled_type higher_order pred_sym ary =

   315   ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order

   317 fun mangled_const_name T_args (s, s') =

   318   let

   319     val ty_args = map (fo_term_from_typ false) T_args

   320     fun type_suffix f g =

   321       fold_rev (curry (op ^) o g o prefix mangled_type_sep

   322                 o generic_mangled_type_name f) ty_args ""

   323   in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end

   325 val parse_mangled_ident =

   326   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode

   328 fun parse_mangled_type x =

   329   (parse_mangled_ident

   330    -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")

   331                     [] >> ATerm) x

   332 and parse_mangled_types x =

   333   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x

   335 fun unmangled_type s =

   336   s |> suffix ")" |> raw_explode

   337     |> Scan.finite Symbol.stopper

   338            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^

   339                                                 quote s)) parse_mangled_type))

   340     |> fst

   342 val unmangled_const_name = space_explode mangled_type_sep #> hd

   343 fun unmangled_const s =

   344   let val ss = space_explode mangled_type_sep s in

   345     (hd ss, map unmangled_type (tl ss))

   346   end

   348 fun introduce_proxies format type_sys =

   349   let

   350     fun intro top_level (CombApp (tm1, tm2)) =

   351         CombApp (intro top_level tm1, intro false tm2)

   352       | intro top_level (CombConst (name as (s, _), T, T_args)) =

   353         (case proxify_const s of

   354            SOME (_, proxy_base) =>

   355            if top_level orelse is_setting_higher_order format type_sys then

   356              case (top_level, s) of

   357                (_, "c_False") => (`I tptp_false, [])

   358              | (_, "c_True") => (`I tptp_true, [])

   359              | (false, "c_Not") => (`I tptp_not, [])

   360              | (false, "c_conj") => (`I tptp_and, [])

   361              | (false, "c_disj") => (`I tptp_or, [])

   362              | (false, "c_implies") => (`I tptp_implies, [])

   363              | (false, s) =>

   364                if is_tptp_equal s then (`I tptp_equal, [])

   365                else (proxy_base |>> prefix const_prefix, T_args)

   366              | _ => (name, [])

   367            else

   368              (proxy_base |>> prefix const_prefix, T_args)

   369           | NONE => (name, T_args))

   370         |> (fn (name, T_args) => CombConst (name, T, T_args))

   371       | intro _ tm = tm

   372   in intro true end

   374 fun combformula_from_prop thy format type_sys eq_as_iff =

   375   let

   376     fun do_term bs t atomic_types =

   377       combterm_from_term thy bs (Envir.eta_contract t)

   378       |>> (introduce_proxies format type_sys #> AAtom)

   379       ||> union (op =) atomic_types

   380     fun do_quant bs q s T t' =

   381       let val s = Name.variant (map fst bs) s in

   382         do_formula ((s, T) :: bs) t'

   383         #>> mk_aquant q [(`make_bound_var s, SOME T)]

   384       end

   385     and do_conn bs c t1 t2 =

   386       do_formula bs t1 ##>> do_formula bs t2

   387       #>> uncurry (mk_aconn c)

   388     and do_formula bs t =

   389       case t of

   390         @{const Not} $ t1 => do_formula bs t1 #>> mk_anot

   391       | Const (@{const_name All}, _) $ Abs (s, T, t') =>

   392         do_quant bs AForall s T t'

   393       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>

   394         do_quant bs AExists s T t'

   395       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2

   396       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2

   397       | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2

   398       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>

   399         if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t

   400       | _ => do_term bs t

   401   in do_formula [] end

   403 fun presimplify_term ctxt =

   404   Skip_Proof.make_thm (Proof_Context.theory_of ctxt)

   405   #> Meson.presimplify ctxt

   406   #> prop_of

   408 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j

   409 fun conceal_bounds Ts t =

   410   subst_bounds (map (Free o apfst concealed_bound_name)

   411                     (0 upto length Ts - 1 ~~ Ts), t)

   412 fun reveal_bounds Ts =

   413   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))

   414                     (0 upto length Ts - 1 ~~ Ts))

   416 fun extensionalize_term ctxt t =

   417   let val thy = Proof_Context.theory_of ctxt in

   418     t |> cterm_of thy |> Meson.extensionalize_conv ctxt

   419       |> prop_of |> Logic.dest_equals |> snd

   420   end

   422 fun introduce_combinators_in_term ctxt kind t =

   423   let val thy = Proof_Context.theory_of ctxt in

   424     if Meson.is_fol_term thy t then

   425       t

   426     else

   427       let

   428         fun aux Ts t =

   429           case t of

   430             @{const Not} $ t1 => @{const Not} $ aux Ts t1

   431           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>

   432             t0 $ Abs (s, T, aux (T :: Ts) t')

   433           | (t0 as Const (@{const_name All}, _)) $ t1 =>

   434             aux Ts (t0 $ eta_expand Ts t1 1)

   435           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>

   436             t0 $ Abs (s, T, aux (T :: Ts) t')

   437           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>

   438             aux Ts (t0 $ eta_expand Ts t1 1)

   439           | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

   440           | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

   441           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

   442           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))

   443               $ t1 $ t2 =>

   444             t0 $ aux Ts t1 $ aux Ts t2

   445           | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then

   446                    t

   447                  else

   448                    t |> conceal_bounds Ts

   449                      |> Envir.eta_contract

   450                      |> cterm_of thy

   451                      |> Meson_Clausify.introduce_combinators_in_cterm

   452                      |> prop_of |> Logic.dest_equals |> snd

   453                      |> reveal_bounds Ts

   454         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single

   455       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end

   456       handle THM _ =>

   457              (* A type variable of sort "{}" will make abstraction fail. *)

   458              if kind = Conjecture then HOLogic.false_const

   459              else HOLogic.true_const

   460   end

   462 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the

   463    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)

   464 fun freeze_term t =

   465   let

   466     fun aux (t $ u) = aux t $ aux u

   467       | aux (Abs (s, T, t)) = Abs (s, T, aux t)

   468       | aux (Var ((s, i), T)) =

   469         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)

   470       | aux t = t

   471   in t |> exists_subterm is_Var t ? aux end

   473 (* making fact and conjecture formulas *)

   474 fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t =

   475   let

   476     val thy = Proof_Context.theory_of ctxt

   477     val t = t |> Envir.beta_eta_contract

   478               |> transform_elim_prop

   479               |> Object_Logic.atomize_term thy

   480     val need_trueprop = (fastype_of t = @{typ bool})

   481     val t = t |> need_trueprop ? HOLogic.mk_Trueprop

   482               |> Raw_Simplifier.rewrite_term thy

   483                      (Meson.unfold_set_const_simps ctxt) []

   484               |> extensionalize_term ctxt

   485               |> presimp ? presimplify_term ctxt

   486               |> perhaps (try (HOLogic.dest_Trueprop))

   487               |> introduce_combinators_in_term ctxt kind

   488               |> kind <> Axiom ? freeze_term

   489     val (combformula, atomic_types) =

   490       combformula_from_prop thy format type_sys eq_as_iff t []

   491   in

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

   493      atomic_types = atomic_types}

   494   end

   496 fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp

   497               ((name, loc), t) =

   498   case (keep_trivial,

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

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

   501     if s = tptp_true then NONE else SOME formula

   502   | (_, formula) => SOME formula

   504 fun make_conjecture ctxt format prem_kind type_sys ts =

   505   let val last = length ts - 1 in

   506     map2 (fn j => fn t =>

   507              let

   508                val (kind, maybe_negate) =

   509                  if j = last then

   510                    (Conjecture, I)

   511                  else

   512                    (prem_kind,

   513                     if prem_kind = Conjecture then update_combformula mk_anot

   514                     else I)

   515               in

   516                 t |> make_formula ctxt format type_sys true true

   517                                   (string_of_int j) General kind

   518                   |> maybe_negate

   519               end)

   520          (0 upto last) ts

   521   end

   523 (** Finite and infinite type inference **)

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

   526   | deep_freeze_atyp T = T

   527 val deep_freeze_type = map_atyps deep_freeze_atyp

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

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

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

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

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

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

   536   | should_encode_type _ _ All_Types _ = true

   537   | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T

   538   | should_encode_type _ _ _ _ = false

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

   541                              should_predicate_on_var T =

   542     (heaviness = Heavy orelse should_predicate_on_var ()) andalso

   543     should_encode_type ctxt nonmono_Ts level T

   544   | should_predicate_on_type _ _ _ _ _ = false

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

   547     String.isPrefix bound_var_prefix s

   548   | is_var_or_bound_var (CombVar _) = true

   549   | is_var_or_bound_var _ = false

   551 datatype tag_site = Top_Level | Eq_Arg | Elsewhere

   553 fun should_tag_with_type _ _ _ Top_Level _ _ = false

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

   555     (case heaviness of

   556        Heavy => should_encode_type ctxt nonmono_Ts level T

   557      | Light =>

   558        case (site, is_var_or_bound_var u) of

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

   560        | _ => false)

   561   | should_tag_with_type _ _ _ _ _ _ = false

   563 fun homogenized_type ctxt nonmono_Ts level =

   564   let

   565     val should_encode = should_encode_type ctxt nonmono_Ts level

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

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

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

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

   570   in homo end

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

   574 type sym_info =

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

   577 fun add_combterm_syms_to_table ctxt explicit_apply =

   578   let

   579     fun consider_var_arity const_T var_T max_ary =

   580       let

   581         fun iter ary T =

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

   583           else iter (ary + 1) (range_type T)

   584       in iter 0 const_T end

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

   586       let val (head, args) = strip_combterm_comb tm in

   587         (case head of

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

   589            if String.isPrefix bound_var_prefix s then

   590              if explicit_apply = NONE andalso can dest_funT T then

   591                let

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

   593                    {pred_sym = pred_sym,

   594                     min_ary =

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

   596                     max_ary = max_ary, types = types}

   597                  val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T

   598                in

   599                  if pointer_eq (ho_var_Ts', ho_var_Ts) then accum

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

   601                end

   602              else

   603                accum

   604            else

   605              let

   606                val ary = length args

   607              in

   608                (ho_var_Ts,

   609                 case Symtab.lookup sym_tab s of

   610                   SOME {pred_sym, min_ary, max_ary, types} =>

   611                   let

   612                     val types' = types |> insert_type ctxt I T

   613                     val min_ary =

   614                       if is_some explicit_apply orelse

   615                          pointer_eq (types', types) then

   616                         min_ary

   617                       else

   618                         fold (consider_var_arity T) ho_var_Ts min_ary

   619                   in

   620                     Symtab.update (s, {pred_sym = pred_sym andalso top_level,

   621                                        min_ary = Int.min (ary, min_ary),

   622                                        max_ary = Int.max (ary, max_ary),

   623                                        types = types'})

   624                                   sym_tab

   625                   end

   626                 | NONE =>

   627                   let

   628                     val min_ary =

   629                       case explicit_apply of

   630                         SOME true => 0

   631                       | SOME false => ary

   632                       | NONE => fold (consider_var_arity T) ho_var_Ts ary

   633                   in

   634                     Symtab.update_new (s, {pred_sym = top_level,

   635                                            min_ary = min_ary, max_ary = ary,

   636                                            types = [T]})

   637                                       sym_tab

   638                   end)

   639              end

   640          | _ => accum)

   641         |> fold (add false) args

   642       end

   643   in add true end

   644 fun add_fact_syms_to_table ctxt explicit_apply =

   645   fact_lift (formula_fold NONE

   646                           (K (add_combterm_syms_to_table ctxt explicit_apply)))

   648 val default_sym_table_entries : (string * sym_info) list =

   649   [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),

   650    (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),

   651    (make_fixed_const predicator_name,

   652     {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @

   653   ([tptp_false, tptp_true]

   654    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []}))

   656 fun sym_table_for_facts ctxt explicit_apply facts =

   657   Symtab.empty

   658   |> fold Symtab.default default_sym_table_entries

   659   |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd

   661 fun min_arity_of sym_tab s =

   662   case Symtab.lookup sym_tab s of

   663     SOME ({min_ary, ...} : sym_info) => min_ary

   664   | NONE =>

   665     case strip_prefix_and_unascii const_prefix s of

   666       SOME s =>

   667       let val s = s |> unmangled_const_name |> invert_const in

   668         if s = predicator_name then 1

   669         else if s = app_op_name then 2

   670         else if s = type_pred_name then 1

   671         else 0

   672       end

   673     | NONE => 0

   675 (* True if the constant ever appears outside of the top-level position in

   676    literals, or if it appears with different arities (e.g., because of different

   677    type instantiations). If false, the constant always receives all of its

   678    arguments and is used as a predicate. *)

   679 fun is_pred_sym sym_tab s =

   680   case Symtab.lookup sym_tab s of

   681     SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>

   682     pred_sym andalso min_ary = max_ary

   683   | NONE => false

   685 val predicator_combconst =

   686   CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])

   687 fun predicator tm = CombApp (predicator_combconst, tm)

   689 fun introduce_predicators_in_combterm sym_tab tm =

   690   case strip_combterm_comb tm of

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

   692     if is_pred_sym sym_tab s then tm else predicator tm

   693   | _ => predicator tm

   695 fun list_app head args = fold (curry (CombApp o swap)) args head

   697 fun explicit_app arg head =

   698   let

   699     val head_T = combtyp_of head

   700     val (arg_T, res_T) = dest_funT head_T

   701     val explicit_app =

   702       CombConst (`make_fixed_const app_op_name, head_T --> head_T,

   703                  [arg_T, res_T])

   704   in list_app explicit_app [head, arg] end

   705 fun list_explicit_app head args = fold explicit_app args head

   707 fun introduce_explicit_apps_in_combterm sym_tab =

   708   let

   709     fun aux tm =

   710       case strip_combterm_comb tm of

   711         (head as CombConst ((s, _), _, _), args) =>

   712         args |> map aux

   713              |> chop (min_arity_of sym_tab s)

   714              |>> list_app head

   715              |-> list_explicit_app

   716       | (head, args) => list_explicit_app head (map aux args)

   717   in aux end

   719 fun chop_fun 0 T = ([], T)

   720   | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =

   721     chop_fun (n - 1) ran_T |>> cons dom_T

   722   | chop_fun _ _ = raise Fail "unexpected non-function"

   724 fun filter_type_args _ _ _ [] = []

   725   | filter_type_args thy s arity T_args =

   726     let

   727       (* will throw "TYPE" for pseudo-constants *)

   728       val U = if s = app_op_name then

   729                 @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global

   730               else

   731                 s |> Sign.the_const_type thy

   732     in

   733       case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of

   734         [] => []

   735       | res_U_vars =>

   736         let val U_args = (s, U) |> Sign.const_typargs thy in

   737           U_args ~~ T_args

   738           |> map_filter (fn (U, T) =>

   739                             if member (op =) res_U_vars (dest_TVar U) then

   740                               SOME T

   741                             else

   742                               NONE)

   743         end

   744     end

   745     handle TYPE _ => T_args

   747 fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =

   748   let

   749     val thy = Proof_Context.theory_of ctxt

   750     fun aux arity (CombApp (tm1, tm2)) =

   751         CombApp (aux (arity + 1) tm1, aux 0 tm2)

   752       | aux arity (CombConst (name as (s, _), T, T_args)) =

   753         let

   754           val level = level_of_type_sys type_sys

   755           val (T, T_args) =

   756             (* Aggressively merge most "hAPPs" if the type system is unsound

   757                anyway, by distinguishing overloads only on the homogenized

   758                result type. Don't do it for lightweight type systems, though,

   759                since it leads to too many unsound proofs. *)

   760             if s = const_prefix ^ app_op_name andalso

   761                length T_args = 2 andalso

   762                not (is_type_sys_virtually_sound type_sys) andalso

   763                heaviness_of_type_sys type_sys = Heavy then

   764               T_args |> map (homogenized_type ctxt nonmono_Ts level 0)

   765                      |> (fn Ts => let val T = hd Ts --> nth Ts 1 in

   766                                     (T --> T, tl Ts)

   767                                   end)

   768             else

   769               (T, T_args)

   770         in

   771           (case strip_prefix_and_unascii const_prefix s of

   772              NONE => (name, T_args)

   773            | SOME s'' =>

   774              let

   775                val s'' = invert_const s''

   776                fun filtered_T_args false = T_args

   777                  | filtered_T_args true = filter_type_args thy s'' arity T_args

   778              in

   779                case type_arg_policy type_sys s'' of

   780                  Explicit_Type_Args drop_args =>

   781                  (name, filtered_T_args drop_args)

   782                | Mangled_Type_Args drop_args =>

   783                  (mangled_const_name (filtered_T_args drop_args) name, [])

   784                | No_Type_Args => (name, [])

   785              end)

   786           |> (fn (name, T_args) => CombConst (name, T, T_args))

   787         end

   788       | aux _ tm = tm

   789   in aux 0 end

   791 fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab =

   792   not (is_setting_higher_order format type_sys)

   793   ? (introduce_explicit_apps_in_combterm sym_tab

   794      #> introduce_predicators_in_combterm sym_tab)

   795   #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys

   796 fun repair_fact ctxt format nonmono_Ts type_sys sym_tab =

   797   update_combformula (formula_map

   798       (repair_combterm ctxt format nonmono_Ts type_sys sym_tab))

   800 (** Helper facts **)

   802 fun ti_ti_helper_fact () =

   803   let

   804     fun var s = ATerm (`I s, [])

   805     fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])

   806   in

   807     Formula (helper_prefix ^ "ti_ti", Axiom,

   808              AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")]))

   809              |> close_formula_universally, simp_info, NONE)

   810   end

   812 fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =

   813   case strip_prefix_and_unascii const_prefix s of

   814     SOME mangled_s =>

   815     let

   816       val thy = Proof_Context.theory_of ctxt

   817       val unmangled_s = mangled_s |> unmangled_const_name

   818       fun dub_and_inst c needs_fairly_sound (th, j) =

   819         ((c ^ "_" ^ string_of_int j ^

   820           (if needs_fairly_sound then typed_helper_suffix

   821            else untyped_helper_suffix),

   822           General),

   823          let val t = th |> prop_of in

   824            t |> ((case general_type_arg_policy type_sys of

   825                     Mangled_Type_Args _ => true

   826                   | _ => false) andalso

   827                  not (null (Term.hidden_polymorphism t)))

   828                 ? (case types of

   829                      [T] => specialize_type thy (invert_const unmangled_s, T)

   830                    | _ => I)

   831          end)

   832       fun make_facts eq_as_iff =

   833         map_filter (make_fact ctxt format type_sys false eq_as_iff false)

   834       val fairly_sound = is_type_sys_fairly_sound type_sys

   835     in

   836       metis_helpers

   837       |> maps (fn (metis_s, (needs_fairly_sound, ths)) =>

   838                   if metis_s <> unmangled_s orelse

   839                      (needs_fairly_sound andalso not fairly_sound) then

   840                     []

   841                   else

   842                     ths ~~ (1 upto length ths)

   843                     |> map (dub_and_inst mangled_s needs_fairly_sound)

   844                     |> make_facts (not needs_fairly_sound))

   845     end

   846   | NONE => []

   847 fun helper_facts_for_sym_table ctxt format type_sys sym_tab =

   848   Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab

   849                   []

   851 fun translate_atp_fact ctxt format type_sys keep_trivial =

   852   `(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of)

   854 fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t

   855                        rich_facts =

   856   let

   857     val thy = Proof_Context.theory_of ctxt

   858     val fact_ts = map (prop_of o snd o snd) rich_facts

   859     val (facts, fact_names) =

   860       rich_facts

   861       |> map_filter (fn (NONE, _) => NONE

   862                       | (SOME fact, (name, _)) => SOME (fact, name))

   863       |> ListPair.unzip

   864     (* Remove existing facts from the conjecture, as this can dramatically

   865        boost an ATP's performance (for some reason). *)

   866     val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)

   867     val goal_t = Logic.list_implies (hyp_ts, concl_t)

   868     val all_ts = goal_t :: fact_ts

   869     val subs = tfree_classes_of_terms all_ts

   870     val supers = tvar_classes_of_terms all_ts

   871     val tycons = type_consts_of_terms thy all_ts

   872     val conjs =

   873       hyp_ts @ [concl_t] |> make_conjecture ctxt format prem_kind type_sys

   874     val (supers', arity_clauses) =

   875       if level_of_type_sys type_sys = No_Types then ([], [])

   876       else make_arity_clauses thy tycons supers

   877     val class_rel_clauses = make_class_rel_clauses thy subs supers'

   878   in

   879     (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))

   880   end

   882 fun fo_literal_from_type_literal (TyLitVar (class, name)) =

   883     (true, ATerm (class, [ATerm (name, [])]))

   884   | fo_literal_from_type_literal (TyLitFree (class, name)) =

   885     (true, ATerm (class, [ATerm (name, [])]))

   887 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot

   889 fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =

   890   CombApp (CombConst (`make_fixed_const type_pred_name, T --> @{typ bool}, [T])

   891            |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,

   892            tm)

   894 fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum

   895   | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =

   896     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))

   897 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false

   898   | is_var_nonmonotonic_in_formula pos phi _ name =

   899     formula_fold pos (var_occurs_positively_naked_in_term name) phi false

   901 fun mk_const_aterm x T_args args =

   902   ATerm (x, map (fo_term_from_typ false) T_args @ args)

   904 fun tag_with_type ctxt format nonmono_Ts type_sys T tm =

   905   CombConst (`make_fixed_const type_tag_name, T --> T, [T])

   906   |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys

   907   |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level

   908   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))

   909 and term_from_combterm ctxt format nonmono_Ts type_sys =

   910   let

   911     fun aux site u =

   912       let

   913         val (head, args) = strip_combterm_comb u

   914         val (x as (s, _), T_args) =

   915           case head of

   916             CombConst (name, _, T_args) => (name, T_args)

   917           | CombVar (name, _) => (name, [])

   918           | CombApp _ => raise Fail "impossible \"CombApp\""

   919         val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg

   920                        else Elsewhere

   921         val t = mk_const_aterm x T_args (map (aux arg_site) args)

   922         val T = combtyp_of u

   923       in

   924         t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then

   925                 tag_with_type ctxt format nonmono_Ts type_sys T

   926               else

   927                 I)

   928       end

   929   in aux end

   930 and formula_from_combformula ctxt format nonmono_Ts type_sys

   931                              should_predicate_on_var =

   932   let

   933     val higher_order = is_setting_higher_order format type_sys

   934     val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level

   935     val do_bound_type =

   936       case type_sys of

   937         Simple_Types level =>

   938         homogenized_type ctxt nonmono_Ts level 0

   939         #> mangled_type higher_order false 0 #> SOME

   940       | _ => K NONE

   941     fun do_out_of_bound_type pos phi universal (name, T) =

   942       if should_predicate_on_type ctxt nonmono_Ts type_sys

   943              (fn () => should_predicate_on_var pos phi universal name) T then

   944         CombVar (name, T)

   945         |> type_pred_combterm ctxt nonmono_Ts type_sys T

   946         |> do_term |> AAtom |> SOME

   947       else

   948         NONE

   949     fun do_formula pos (AQuant (q, xs, phi)) =

   950         let

   951           val phi = phi |> do_formula pos

   952           val universal = Option.map (q = AExists ? not) pos

   953         in

   954           AQuant (q, xs |> map (apsnd (fn NONE => NONE

   955                                         | SOME T => do_bound_type T)),

   956                   (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))

   957                       (map_filter

   958                            (fn (_, NONE) => NONE

   959                              | (s, SOME T) =>

   960                                do_out_of_bound_type pos phi universal (s, T))

   961                            xs)

   962                       phi)

   963         end

   964       | do_formula pos (AConn conn) = aconn_map pos do_formula conn

   965       | do_formula _ (AAtom tm) = AAtom (do_term tm)

   966   in do_formula o SOME end

   968 fun bound_atomic_types format type_sys Ts =

   969   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)

   970                 (atp_type_literals_for_types format type_sys Axiom Ts))

   972 fun formula_for_fact ctxt format nonmono_Ts type_sys

   973                      ({combformula, atomic_types, ...} : translated_formula) =

   974   combformula

   975   |> close_combformula_universally

   976   |> formula_from_combformula ctxt format nonmono_Ts type_sys

   977                               is_var_nonmonotonic_in_formula true

   978   |> bound_atomic_types format type_sys atomic_types

   979   |> close_formula_universally

   981 (* Each fact is given a unique fact number to avoid name clashes (e.g., because

   982    of monomorphization). The TPTP explicitly forbids name clashes, and some of

   983    the remote provers might care. *)

   984 fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys

   985                           (j, formula as {name, locality, kind, ...}) =

   986   Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""

   987                      else string_of_int j ^ "_") ^

   988            ascii_of name,

   989            kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,

   990            case locality of

   991              Intro => intro_info

   992            | Elim => elim_info

   993            | Simp => simp_info

   994            | _ => NONE)

   996 fun formula_line_for_class_rel_clause

   997         (ClassRelClause {name, subclass, superclass, ...}) =

   998   let val ty_arg = ATerm (`I "T", []) in

   999     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,

  1000              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),

  1001                                AAtom (ATerm (superclass, [ty_arg]))])

  1002              |> close_formula_universally, intro_info, NONE)

  1003   end

  1005 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =

  1006     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))

  1007   | fo_literal_from_arity_literal (TVarLit (c, sort)) =

  1008     (false, ATerm (c, [ATerm (sort, [])]))

  1010 fun formula_line_for_arity_clause

  1011         (ArityClause {name, prem_lits, concl_lits, ...}) =

  1012   Formula (arity_clause_prefix ^ ascii_of name, Axiom,

  1013            mk_ahorn (map (formula_from_fo_literal o apfst not

  1014                           o fo_literal_from_arity_literal) prem_lits)

  1015                     (formula_from_fo_literal

  1016                          (fo_literal_from_arity_literal concl_lits))

  1017            |> close_formula_universally, intro_info, NONE)

  1019 fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys

  1020         ({name, kind, combformula, ...} : translated_formula) =

  1021   Formula (conjecture_prefix ^ name, kind,

  1022            formula_from_combformula ctxt format nonmono_Ts type_sys

  1023                is_var_nonmonotonic_in_formula false

  1024                (close_combformula_universally combformula)

  1025            |> close_formula_universally, NONE, NONE)

  1027 fun free_type_literals format type_sys

  1028                        ({atomic_types, ...} : translated_formula) =

  1029   atomic_types |> atp_type_literals_for_types format type_sys Conjecture

  1030                |> map fo_literal_from_type_literal

  1032 fun formula_line_for_free_type j lit =

  1033   Formula (tfree_prefix ^ string_of_int j, Hypothesis,

  1034            formula_from_fo_literal lit, NONE, NONE)

  1035 fun formula_lines_for_free_types format type_sys facts =

  1036   let

  1037     val litss = map (free_type_literals format type_sys) facts

  1038     val lits = fold (union (op =)) litss []

  1039   in map2 formula_line_for_free_type (0 upto length lits - 1) lits end

  1041 (** Symbol declarations **)

  1043 fun should_declare_sym type_sys pred_sym s =

  1044   is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso

  1045   (case type_sys of

  1046      Simple_Types _ => true

  1047    | Tags (_, _, Light) => true

  1048    | _ => not pred_sym)

  1050 fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =

  1051   let

  1052     fun add_combterm in_conj tm =

  1053       let val (head, args) = strip_combterm_comb tm in

  1054         (case head of

  1055            CombConst ((s, s'), T, T_args) =>

  1056            let val pred_sym = is_pred_sym repaired_sym_tab s in

  1057              if should_declare_sym type_sys pred_sym s then

  1058                Symtab.map_default (s, [])

  1059                    (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,

  1060                                          in_conj))

  1061              else

  1062                I

  1063            end

  1064          | _ => I)

  1065         #> fold (add_combterm in_conj) args

  1066       end

  1067     fun add_fact in_conj =

  1068       fact_lift (formula_fold NONE (K (add_combterm in_conj)))

  1069   in

  1070     Symtab.empty

  1071     |> is_type_sys_fairly_sound type_sys

  1072        ? (fold (add_fact true) conjs #> fold (add_fact false) facts)

  1073   end

  1075 (* These types witness that the type classes they belong to allow infinite

  1076    models and hence that any types with these type classes is monotonic. *)

  1077 val known_infinite_types = [@{typ nat}, @{typ int}, @{typ "nat => bool"}]

  1079 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it

  1080    out with monotonicity" paper presented at CADE 2011. *)

  1081 fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I

  1082   | add_combterm_nonmonotonic_types ctxt level _

  1083         (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =

  1084     (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso

  1085      (case level of

  1086         Nonmonotonic_Types =>

  1087         not (is_type_surely_infinite ctxt known_infinite_types T)

  1088       | Finite_Types => is_type_surely_finite ctxt T

  1089       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)

  1090   | add_combterm_nonmonotonic_types _ _ _ _ = I

  1091 fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...}

  1092                                             : translated_formula) =

  1093   formula_fold (SOME (kind <> Conjecture))

  1094                (add_combterm_nonmonotonic_types ctxt level) combformula

  1095 fun nonmonotonic_types_for_facts ctxt type_sys facts =

  1096   let val level = level_of_type_sys type_sys in

  1097     if level = Nonmonotonic_Types orelse level = Finite_Types then

  1098       [] |> fold (add_fact_nonmonotonic_types ctxt level) facts

  1099          (* We must add "bool" in case the helper "True_or_False" is added

  1100             later. In addition, several places in the code rely on the list of

  1101             nonmonotonic types not being empty. *)

  1102          |> insert_type ctxt I @{typ bool}

  1103     else

  1104       []

  1105   end

  1107 fun decl_line_for_sym ctxt format nonmono_Ts type_sys s

  1108                       (s', T_args, T, pred_sym, ary, _) =

  1109   let

  1110     val (higher_order, T_arg_Ts, level) =

  1111       case type_sys of

  1112         Simple_Types level => (format = THF, [], level)

  1113       | _ => (false, replicate (length T_args) homo_infinite_type, No_Types)

  1114   in

  1115     Decl (sym_decl_prefix ^ s, (s, s'),

  1116           (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))

  1117           |> mangled_type higher_order pred_sym (length T_arg_Ts + ary))

  1118   end

  1120 fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false

  1122 fun formula_line_for_pred_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys

  1123                                    n s j (s', T_args, T, _, ary, in_conj) =

  1124   let

  1125     val (kind, maybe_negate) =

  1126       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)

  1127       else (Axiom, I)

  1128     val (arg_Ts, res_T) = chop_fun ary T

  1129     val bound_names =

  1130       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)

  1131     val bounds =

  1132       bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))

  1133     val bound_Ts =

  1134       arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T

  1135                              else NONE)

  1136   in

  1137     Formula (sym_formula_prefix ^ s ^

  1138              (if n > 1 then "_" ^ string_of_int j else ""), kind,

  1139              CombConst ((s, s'), T, T_args)

  1140              |> fold (curry (CombApp o swap)) bounds

  1141              |> type_pred_combterm ctxt nonmono_Ts type_sys res_T

  1142              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)

  1143              |> formula_from_combformula ctxt format nonmono_Ts type_sys

  1144                                          (K (K (K (K true)))) true

  1145              |> n > 1 ? bound_atomic_types format type_sys (atyps_of T)

  1146              |> close_formula_universally

  1147              |> maybe_negate,

  1148              intro_info, NONE)

  1149   end

  1151 fun formula_lines_for_tag_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys

  1152         n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =

  1153   let

  1154     val ident_base =

  1155       sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")

  1156     val (kind, maybe_negate) =

  1157       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)

  1158       else (Axiom, I)

  1159     val (arg_Ts, res_T) = chop_fun ary T

  1160     val bound_names =

  1161       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)

  1162     val bounds = bound_names |> map (fn name => ATerm (name, []))

  1163     val cst = mk_const_aterm (s, s') T_args

  1164     val atomic_Ts = atyps_of T

  1165     fun eq tms =

  1166       (if pred_sym then AConn (AIff, map AAtom tms)

  1167        else AAtom (ATerm (`I tptp_equal, tms)))

  1168       |> bound_atomic_types format type_sys atomic_Ts

  1169       |> close_formula_universally

  1170       |> maybe_negate

  1171     val should_encode = should_encode_type ctxt nonmono_Ts All_Types

  1172     val tag_with = tag_with_type ctxt format nonmono_Ts type_sys

  1173     val add_formula_for_res =

  1174       if should_encode res_T then

  1175         cons (Formula (ident_base ^ "_res", kind,

  1176                        eq [tag_with res_T (cst bounds), cst bounds],

  1177                        simp_info, NONE))

  1178       else

  1179         I

  1180     fun add_formula_for_arg k =

  1181       let val arg_T = nth arg_Ts k in

  1182         if should_encode arg_T then

  1183           case chop k bounds of

  1184             (bounds1, bound :: bounds2) =>

  1185             cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,

  1186                            eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),

  1187                                cst bounds],

  1188                            simp_info, NONE))

  1189           | _ => raise Fail "expected nonempty tail"

  1190         else

  1191           I

  1192       end

  1193   in

  1194     [] |> not pred_sym ? add_formula_for_res

  1195        |> fold add_formula_for_arg (ary - 1 downto 0)

  1196   end

  1198 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd

  1200 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys

  1201                                 (s, decls) =

  1202   case type_sys of

  1203     Simple_Types _ =>

  1204     decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)

  1205   | Preds _ =>

  1206     let

  1207       val decls =

  1208         case decls of

  1209           decl :: (decls' as _ :: _) =>

  1210           let val T = result_type_of_decl decl in

  1211             if forall (curry (type_instance ctxt o swap) T

  1212                        o result_type_of_decl) decls' then

  1213               [decl]

  1214             else

  1215               decls

  1216           end

  1217         | _ => decls

  1218       val n = length decls

  1219       val decls =

  1220         decls

  1221         |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)

  1222                    o result_type_of_decl)

  1223     in

  1224       (0 upto length decls - 1, decls)

  1225       |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind

  1226                                                nonmono_Ts type_sys n s)

  1227     end

  1228   | Tags (_, _, heaviness) =>

  1229     (case heaviness of

  1230        Heavy => []

  1231      | Light =>

  1232        let val n = length decls in

  1233          (0 upto n - 1 ~~ decls)

  1234          |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind

  1235                                                  nonmono_Ts type_sys n s)

  1236        end)

  1238 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts

  1239                                      type_sys sym_decl_tab =

  1240   sym_decl_tab

  1241   |> Symtab.dest

  1242   |> sort_wrt fst

  1243   |> rpair []

  1244   |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind

  1245                                                      nonmono_Ts type_sys)

  1247 fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =

  1248     level = Nonmonotonic_Types orelse level = Finite_Types

  1249   | should_add_ti_ti_helper _ = false

  1251 fun offset_of_heading_in_problem _ [] j = j

  1252   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =

  1253     if heading = needle then j

  1254     else offset_of_heading_in_problem needle problem (j + length lines)

  1256 val implicit_declsN = "Should-be-implicit typings"

  1257 val explicit_declsN = "Explicit typings"

  1258 val factsN = "Relevant facts"

  1259 val class_relsN = "Class relationships"

  1260 val aritiesN = "Arities"

  1261 val helpersN = "Helper facts"

  1262 val conjsN = "Conjectures"

  1263 val free_typesN = "Type variables"

  1265 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys

  1266                         explicit_apply hyp_ts concl_t facts =

  1267   let

  1268     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =

  1269       translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts

  1270     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply

  1271     val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys

  1272     val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab

  1273     val (conjs, facts) = (conjs, facts) |> pairself (map repair)

  1274     val repaired_sym_tab =

  1275       conjs @ facts |> sym_table_for_facts ctxt (SOME false)

  1276     val helpers =

  1277       repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys

  1278                        |> map repair

  1279     val lavish_nonmono_Ts =

  1280       if null nonmono_Ts orelse

  1281          polymorphism_of_type_sys type_sys <> Polymorphic then

  1282         nonmono_Ts

  1283       else

  1284         [TVar (("'a", 0), HOLogic.typeS)]

  1285     val sym_decl_lines =

  1286       (conjs, helpers @ facts)

  1287       |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab

  1288       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind

  1289                                           lavish_nonmono_Ts type_sys

  1290     val helper_lines =

  1291       0 upto length helpers - 1 ~~ helpers

  1292       |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts

  1293                                     type_sys)

  1294       |> (if should_add_ti_ti_helper type_sys then cons (ti_ti_helper_fact ())

  1295           else I)

  1296     (* Reordering these might confuse the proof reconstruction code or the SPASS

  1297        FLOTTER hack. *)

  1298     val problem =

  1299       [(explicit_declsN, sym_decl_lines),

  1300        (factsN,

  1301         map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)

  1302             (0 upto length facts - 1 ~~ facts)),

  1303        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),

  1304        (aritiesN, map formula_line_for_arity_clause arity_clauses),

  1305        (helpersN, helper_lines),

  1306        (conjsN,

  1307         map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)

  1308             conjs),

  1309        (free_typesN,

  1310         formula_lines_for_free_types format type_sys (facts @ conjs))]

  1311     val problem =

  1312       problem

  1313       |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)

  1314       |> (if is_format_typed format then

  1315             declare_undeclared_syms_in_atp_problem type_decl_prefix

  1316                                                    implicit_declsN

  1317           else

  1318             I)

  1319     val (problem, pool) =

  1320       problem |> nice_atp_problem (Config.get ctxt readable_names)

  1321     val helpers_offset = offset_of_heading_in_problem helpersN problem 0

  1322     val typed_helpers =

  1323       map_filter (fn (j, {name, ...}) =>

  1324                      if String.isSuffix typed_helper_suffix name then SOME j

  1325                      else NONE)

  1326                  ((helpers_offset + 1 upto helpers_offset + length helpers)

  1327                   ~~ helpers)

  1328     fun add_sym_arity (s, {min_ary, ...} : sym_info) =

  1329       if min_ary > 0 then

  1330         case strip_prefix_and_unascii const_prefix s of

  1331           SOME s => Symtab.insert (op =) (s, min_ary)

  1332         | NONE => I

  1333       else

  1334         I

  1335   in

  1336     (problem,

  1337      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,

  1338      offset_of_heading_in_problem conjsN problem 0,

  1339      offset_of_heading_in_problem factsN problem 0,

  1340      fact_names |> Vector.fromList,

  1341      typed_helpers,

  1342      Symtab.empty |> Symtab.fold add_sym_arity sym_tab)

  1343   end

  1345 (* FUDGE *)

  1346 val conj_weight = 0.0

  1347 val hyp_weight = 0.1

  1348 val fact_min_weight = 0.2

  1349 val fact_max_weight = 1.0

  1350 val type_info_default_weight = 0.8

  1352 fun add_term_weights weight (ATerm (s, tms)) =

  1353   is_tptp_user_symbol s ? Symtab.default (s, weight)

  1354   #> fold (add_term_weights weight) tms

  1355 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =

  1356     formula_fold NONE (K (add_term_weights weight)) phi

  1357   | add_problem_line_weights _ _ = I

  1359 fun add_conjectures_weights [] = I

  1360   | add_conjectures_weights conjs =

  1361     let val (hyps, conj) = split_last conjs in

  1362       add_problem_line_weights conj_weight conj

  1363       #> fold (add_problem_line_weights hyp_weight) hyps

  1364     end

  1366 fun add_facts_weights facts =

  1367   let

  1368     val num_facts = length facts

  1369     fun weight_of j =

  1370       fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j

  1371                         / Real.fromInt num_facts

  1372   in

  1373     map weight_of (0 upto num_facts - 1) ~~ facts

  1374     |> fold (uncurry add_problem_line_weights)

  1375   end

  1377 (* Weights are from 0.0 (most important) to 1.0 (least important). *)

  1378 fun atp_problem_weights problem =

  1379   let val get = these o AList.lookup (op =) problem in

  1380     Symtab.empty

  1381     |> add_conjectures_weights (get free_typesN @ get conjsN)

  1382     |> add_facts_weights (get factsN)

  1383     |> fold (fold (add_problem_line_weights type_info_default_weight) o get)

  1384             [explicit_declsN, class_relsN, aritiesN]

  1385     |> Symtab.dest

  1386     |> sort (prod_ord Real.compare string_ord o pairself swap)

  1387   end

  1389 end;

author	blanchet
	Mon, 30 May 2011 17:00:38 +0200
changeset 43905	b6e61d22fa61
parent 43880	b967219cec78
permissions	-rw-r--r--