wneuper/isa: src/HOL/Tools/Sledgehammer/sledgehammer.ML@ed65a0777e10

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

     2     Author:     Fabian Immler, TU Muenchen

     3     Author:     Makarius

     4     Author:     Jasmin Blanchette, TU Muenchen

     6 Sledgehammer's heart.

     7 *)

     9 signature SLEDGEHAMMER =

    10 sig

    11   type failure = ATP_Systems.failure

    12   type relevance_override = Sledgehammer_Fact_Filter.relevance_override

    13   type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command

    14   type params =

    15     {debug: bool,

    16      verbose: bool,

    17      overlord: bool,

    18      atps: string list,

    19      full_types: bool,

    20      explicit_apply: bool,

    21      relevance_threshold: real,

    22      relevance_convergence: real,

    23      theory_relevant: bool option,

    24      defs_relevant: bool,

    25      isar_proof: bool,

    26      isar_shrink_factor: int,

    27      timeout: Time.time,

    28      minimize_timeout: Time.time}

    29   type problem =

    30     {subgoal: int,

    31      goal: Proof.context * (thm list * thm),

    32      relevance_override: relevance_override,

    33      axioms: (string * thm) list option}

    34   type prover_result =

    35     {outcome: failure option,

    36      message: string,

    37      pool: string Symtab.table,

    38      used_thm_names: string list,

    39      atp_run_time_in_msecs: int,

    40      output: string,

    41      proof: string,

    42      internal_thm_names: string Vector.vector,

    43      conjecture_shape: int list list}

    44   type prover =

    45     params -> minimize_command -> Time.time -> problem -> prover_result

    47   val dest_dir : string Config.T

    48   val problem_prefix : string Config.T

    49   val measure_runtime : bool Config.T

    50   val kill_atps: unit -> unit

    51   val running_atps: unit -> unit

    52   val messages: int option -> unit

    53   val get_prover_fun : theory -> string -> prover

    54   val run_sledgehammer :

    55     params -> int -> relevance_override -> (string -> minimize_command)

    56     -> Proof.state -> unit

    57   val setup : theory -> theory

    58 end;

    60 structure Sledgehammer : SLEDGEHAMMER =

    61 struct

    63 open ATP_Problem

    64 open ATP_Systems

    65 open Metis_Clauses

    66 open Sledgehammer_Util

    67 open Sledgehammer_Fact_Filter

    68 open Sledgehammer_Proof_Reconstruct

    71 (** The Sledgehammer **)

    73 val das_Tool = "Sledgehammer"

    75 fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"

    76 fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"

    77 val messages = Async_Manager.thread_messages das_Tool "ATP"

    79 (** problems, results, provers, etc. **)

    81 type params =

    82   {debug: bool,

    83    verbose: bool,

    84    overlord: bool,

    85    atps: string list,

    86    full_types: bool,

    87    explicit_apply: bool,

    88    relevance_threshold: real,

    89    relevance_convergence: real,

    90    theory_relevant: bool option,

    91    defs_relevant: bool,

    92    isar_proof: bool,

    93    isar_shrink_factor: int,

    94    timeout: Time.time,

    95    minimize_timeout: Time.time}

    97 type problem =

    98   {subgoal: int,

    99    goal: Proof.context * (thm list * thm),

   100    relevance_override: relevance_override,

   101    axioms: (string * thm) list option}

   103 type prover_result =

   104   {outcome: failure option,

   105    message: string,

   106    pool: string Symtab.table,

   107    used_thm_names: string list,

   108    atp_run_time_in_msecs: int,

   109    output: string,

   110    proof: string,

   111    internal_thm_names: string Vector.vector,

   112    conjecture_shape: int list list}

   114 type prover =

   115   params -> minimize_command -> Time.time -> problem -> prover_result

   117 (* configuration attributes *)

   119 val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");

   120   (*Empty string means create files in Isabelle's temporary files directory.*)

   122 val (problem_prefix, problem_prefix_setup) =

   123   Attrib.config_string "atp_problem_prefix" (K "prob");

   125 val (measure_runtime, measure_runtime_setup) =

   126   Attrib.config_bool "atp_measure_runtime" (K false);

   128 fun with_path cleanup after f path =

   129   Exn.capture f path

   130   |> tap (fn _ => cleanup path)

   131   |> Exn.release

   132   |> tap (after path)

   134 (* Splits by the first possible of a list of delimiters. *)

   135 fun extract_proof delims output =

   136   case pairself (find_first (fn s => String.isSubstring s output))

   137                 (ListPair.unzip delims) of

   138     (SOME begin_delim, SOME end_delim) =>

   139     (output |> first_field begin_delim |> the |> snd

   140             |> first_field end_delim |> the |> fst

   141             |> first_field "\n" |> the |> snd

   142      handle Option.Option => "")

   143   | _ => ""

   145 fun extract_proof_and_outcome complete res_code proof_delims known_failures

   146                               output =

   147   case known_failure_in_output output known_failures of

   148     NONE => (case extract_proof proof_delims output of

   149              "" => ("", SOME MalformedOutput)

   150            | proof => if res_code = 0 then (proof, NONE)

   151                       else ("", SOME UnknownError))

   152   | SOME failure =>

   153     ("", SOME (if failure = IncompleteUnprovable andalso complete then

   154                  Unprovable

   155                else

   156                  failure))

   159 (* Clause preparation *)

   161 datatype fol_formula =

   162   FOLFormula of {formula_name: string,

   163                  kind: kind,

   164                  combformula: (name, combterm) formula,

   165                  ctypes_sorts: typ list}

   167 fun mk_anot phi = AConn (ANot, [phi])

   168 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])

   169 fun mk_ahorn [] phi = phi

   170   | mk_ahorn (phi :: phis) psi =

   171     AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])

   173 (* ### FIXME: reintroduce

   174 fun make_formula_table xs =

   175   fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty

   176 (* Remove existing axioms from the conjecture, as this can

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

   178 fun subtract_cls axioms =

   179   filter_out (Termtab.defined (make_formula_table axioms) o prop_of)

   180 *)

   182 fun combformula_for_prop thy =

   183   let

   184     val do_term = combterm_from_term thy

   185     fun do_quant bs q s T t' =

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

   187       #>> (fn phi => AQuant (q, [`make_bound_var s], phi))

   188     and do_conn bs c t1 t2 =

   189       do_formula bs t1 ##>> do_formula bs t2

   190       #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))

   191     and do_formula bs t =

   192       case t of

   193         @{const Not} $ t1 =>

   194         do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))

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

   196         do_quant bs AForall s T t'

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

   198         do_quant bs AExists s T t'

   199       | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2

   200       | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2

   201       | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2

   202       | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>

   203         do_conn bs AIff t1 t2

   204       | _ => (fn ts => do_term bs (Envir.eta_contract t)

   205                        |>> AAtom ||> union (op =) ts)

   206   in do_formula [] end

   208 (* Converts an elim-rule into an equivalent theorem that does not have the

   209    predicate variable. Leaves other theorems unchanged. We simply instantiate

   210    the conclusion variable to False. (Cf. "transform_elim_term" in

   211    "ATP_Systems".) *)

   212 (* FIXME: test! *)

   213 fun transform_elim_term t =

   214   case Logic.strip_imp_concl t of

   215     @{const Trueprop} $ Var (z, @{typ bool}) =>

   216     subst_Vars [(z, @{const True})] t

   217   | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t

   218   | _ => t

   220 (* Removes the lambdas from an equation of the form "t = (%x. u)".

   221    (Cf. "extensionalize_theorem" in "Clausifier".) *)

   222 fun extensionalize_term t =

   223   let

   224     fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _]))

   225                $ t2 $ Abs (s, var_T, t')) =

   226         let val var_t = Var (("x", j), var_T) in

   227           Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)

   228             $ betapply (t2, var_t) $ subst_bound (var_t, t')

   229           |> aux (j + 1)

   230         end

   231       | aux _ t = t

   232   in aux (maxidx_of_term t + 1) t end

   234 fun presimplify_term thy =

   235   HOLogic.mk_Trueprop

   236   #> Skip_Proof.make_thm thy

   237   #> Meson.presimplify

   238   #> prop_of

   239   #> HOLogic.dest_Trueprop

   241 (* FIXME: Guarantee freshness *)

   242 fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j

   243 fun conceal_bounds Ts t =

   244   subst_bounds (map (Free o apfst concealed_bound_name)

   245                     (length Ts - 1 downto 0 ~~ rev Ts), t)

   246 fun reveal_bounds Ts =

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

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

   250 fun introduce_combinators_in_term ctxt kind t =

   251   let

   252     val thy = ProofContext.theory_of ctxt

   253     fun aux Ts t =

   254       case t of

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

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

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

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

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

   260       | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

   261       | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

   262       | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2

   263       | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))

   264           $ t1 $ t2 =>

   265         t0 $ aux Ts t1 $ aux Ts t2

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

   267                t

   268              else

   269                let

   270                  val t = t |> conceal_bounds Ts

   271                            |> Envir.eta_contract

   272                  val ([t], ctxt') = Variable.import_terms true [t] ctxt

   273                in

   274                  t |> cterm_of thy

   275                    |> Clausifier.introduce_combinators_in_cterm

   276                    |> singleton (Variable.export ctxt' ctxt)

   277                    |> prop_of |> Logic.dest_equals |> snd

   278                    |> reveal_bounds Ts

   279                end

   280   in t |> not (Meson.is_fol_term thy t) ? aux [] end

   281   handle THM _ =>

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

   283          case kind of

   284            Axiom => HOLogic.true_const

   285          | Conjecture => HOLogic.false_const

   287 (* making axiom and conjecture formulas *)

   288 fun make_formula ctxt presimp (formula_name, kind, t) =

   289   let

   290     val thy = ProofContext.theory_of ctxt

   291     val t = t |> transform_elim_term

   292               |> Object_Logic.atomize_term thy

   293               |> extensionalize_term

   294               |> presimp ? presimplify_term thy

   295               |> introduce_combinators_in_term ctxt kind

   296     val (combformula, ctypes_sorts) = combformula_for_prop thy t []

   297   in

   298     FOLFormula {formula_name = formula_name, combformula = combformula,

   299                 kind = kind, ctypes_sorts = ctypes_sorts}

   300   end

   302 fun make_axiom ctxt presimp (name, th) =

   303   (name, make_formula ctxt presimp (name, Axiom, prop_of th))

   304 fun make_conjectures ctxt ts =

   305   map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))

   306        (0 upto length ts - 1) ts

   308 (** Helper facts **)

   310 fun count_combterm (CombConst ((s, _), _, _)) =

   311     Symtab.map_entry s (Integer.add 1)

   312   | count_combterm (CombVar _) = I

   313   | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]

   314 fun count_combformula (AQuant (_, _, phi)) = count_combformula phi

   315   | count_combformula (AConn (_, phis)) = fold count_combformula phis

   316   | count_combformula (AAtom tm) = count_combterm tm

   317 fun count_fol_formula (FOLFormula {combformula, ...}) =

   318   count_combformula combformula

   320 val optional_helpers =

   321   [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),

   322    (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),

   323    (["c_COMBS"], @{thms COMBS_def})]

   324 val optional_typed_helpers =

   325   [(["c_True", "c_False"], @{thms True_or_False}),

   326    (["c_If"], @{thms if_True if_False True_or_False})]

   327 val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}

   329 val init_counters =

   330   Symtab.make (maps (maps (map (rpair 0) o fst))

   331                     [optional_helpers, optional_typed_helpers])

   333 fun get_helper_facts ctxt is_FO full_types conjectures axioms =

   334   let

   335     val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters

   336     fun is_needed c = the (Symtab.lookup ct c) > 0

   337   in

   338     (optional_helpers

   339      |> full_types ? append optional_typed_helpers

   340      |> maps (fn (ss, ths) =>

   341                  if exists is_needed ss then map (`Thm.get_name_hint) ths

   342                  else [])) @

   343     (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)

   344     |> map (snd o make_axiom ctxt false)

   345   end

   347 fun meta_not t = @{const "==>"} $ t $ @{prop False}

   349 fun prepare_formulas ctxt full_types hyp_ts concl_t axcls =

   350   let

   351     val thy = ProofContext.theory_of ctxt

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

   353     val is_FO = Meson.is_fol_term thy goal_t

   354     val axtms = map (prop_of o snd) axcls

   355     val subs = tfree_classes_of_terms [goal_t]

   356     val supers = tvar_classes_of_terms axtms

   357     val tycons = type_consts_of_terms thy (goal_t :: axtms)

   358     (* TFrees in the conjecture; TVars in the axioms *)

   359     val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt

   360     val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt true) axcls)

   361     val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms

   362     val (supers', arity_clauses) = make_arity_clauses thy tycons supers

   363     val class_rel_clauses = make_class_rel_clauses thy subs supers'

   364   in

   365     (Vector.fromList clnames,

   366       (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))

   367   end

   369 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])

   371 fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])

   372   | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])

   373   | fo_term_for_combtyp (CombType (name, tys)) =

   374     ATerm (name, map fo_term_for_combtyp tys)

   376 fun fo_literal_for_type_literal (TyLitVar (class, name)) =

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

   378   | fo_literal_for_type_literal (TyLitFree (class, name)) =

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

   381 fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot

   383 fun fo_term_for_combterm full_types =

   384   let

   385     fun aux top_level u =

   386       let

   387         val (head, args) = strip_combterm_comb u

   388         val (x, ty_args) =

   389           case head of

   390             CombConst (name as (s, s'), _, ty_args) =>

   391             if s = "equal" then

   392               (if top_level andalso length args = 2 then name

   393                else ("c_fequal", @{const_name fequal}), [])

   394             else if top_level then

   395               case s of

   396                 "c_False" => (("$false", s'), [])

   397               | "c_True" => (("$true", s'), [])

   398               | _ => (name, if full_types then [] else ty_args)

   399             else

   400               (name, if full_types then [] else ty_args)

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

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

   403         val t = ATerm (x, map fo_term_for_combtyp ty_args @

   404                           map (aux false) args)

   405     in

   406       if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t

   407     end

   408   in aux true end

   410 fun formula_for_combformula full_types =

   411   let

   412     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)

   413       | aux (AConn (c, phis)) = AConn (c, map aux phis)

   414       | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)

   415   in aux end

   417 fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =

   418   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)

   419                 (type_literals_for_types ctypes_sorts))

   420            (formula_for_combformula full_types combformula)

   422 fun problem_line_for_axiom full_types

   423         (formula as FOLFormula {formula_name, kind, ...}) =

   424   Fof (axiom_prefix ^ ascii_of formula_name, kind,

   425        formula_for_axiom full_types formula)

   427 fun problem_line_for_class_rel_clause

   428         (ClassRelClause {axiom_name, subclass, superclass, ...}) =

   429   let val ty_arg = ATerm (("T", "T"), []) in

   430     Fof (ascii_of axiom_name, Axiom,

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

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

   433   end

   435 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =

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

   437   | fo_literal_for_arity_literal (TVarLit (c, sort)) =

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

   440 fun problem_line_for_arity_clause

   441         (ArityClause {axiom_name, conclLit, premLits, ...}) =

   442   Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,

   443        mk_ahorn (map (formula_for_fo_literal o apfst not

   444                       o fo_literal_for_arity_literal) premLits)

   445                 (formula_for_fo_literal

   446                      (fo_literal_for_arity_literal conclLit)))

   448 fun problem_line_for_conjecture full_types

   449         (FOLFormula {formula_name, kind, combformula, ...}) =

   450   Fof (conjecture_prefix ^ formula_name, kind,

   451        formula_for_combformula full_types combformula)

   453 fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =

   454   map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)

   456 fun problem_line_for_free_type lit =

   457   Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))

   458 fun problem_lines_for_free_types conjectures =

   459   let

   460     val litss = map free_type_literals_for_conjecture conjectures

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

   462   in map problem_line_for_free_type lits end

   464 (** "hBOOL" and "hAPP" **)

   466 type const_info = {min_arity: int, max_arity: int, sub_level: bool}

   468 fun consider_term top_level (ATerm ((s, _), ts)) =

   469   (if is_tptp_variable s then

   470      I

   471    else

   472      let val n = length ts in

   473        Symtab.map_default

   474            (s, {min_arity = n, max_arity = 0, sub_level = false})

   475            (fn {min_arity, max_arity, sub_level} =>

   476                {min_arity = Int.min (n, min_arity),

   477                 max_arity = Int.max (n, max_arity),

   478                 sub_level = sub_level orelse not top_level})

   479      end)

   480   #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts

   481 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi

   482   | consider_formula (AConn (_, phis)) = fold consider_formula phis

   483   | consider_formula (AAtom tm) = consider_term true tm

   485 fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi

   486 fun consider_problem problem = fold (fold consider_problem_line o snd) problem

   488 fun const_table_for_problem explicit_apply problem =

   489   if explicit_apply then NONE

   490   else SOME (Symtab.empty |> consider_problem problem)

   492 val tc_fun = make_fixed_type_const @{type_name fun}

   494 fun min_arity_of thy full_types NONE s =

   495     (if s = "equal" orelse s = type_wrapper_name orelse

   496         String.isPrefix type_const_prefix s orelse

   497         String.isPrefix class_prefix s then

   498        16383 (* large number *)

   499      else if full_types then

   500        0

   501      else case strip_prefix_and_undo_ascii const_prefix s of

   502        SOME s' => num_type_args thy (invert_const s')

   503      | NONE => 0)

   504   | min_arity_of _ _ (SOME the_const_tab) s =

   505     case Symtab.lookup the_const_tab s of

   506       SOME ({min_arity, ...} : const_info) => min_arity

   507     | NONE => 0

   509 fun full_type_of (ATerm ((s, _), [ty, _])) =

   510     if s = type_wrapper_name then ty else raise Fail "expected type wrapper"

   511   | full_type_of _ = raise Fail "expected type wrapper"

   513 fun list_hAPP_rev _ t1 [] = t1

   514   | list_hAPP_rev NONE t1 (t2 :: ts2) =

   515     ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])

   516   | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =

   517     let val ty' = ATerm (`make_fixed_type_const @{type_name fun},

   518                          [full_type_of t2, ty]) in

   519       ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])

   520     end

   522 fun repair_applications_in_term thy full_types const_tab =

   523   let

   524     fun aux opt_ty (ATerm (name as (s, _), ts)) =

   525       if s = type_wrapper_name then

   526         case ts of

   527           [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])

   528         | _ => raise Fail "malformed type wrapper"

   529       else

   530         let

   531           val ts = map (aux NONE) ts

   532           val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts

   533         in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end

   534   in aux NONE end

   536 fun boolify t = ATerm (`I "hBOOL", [t])

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

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

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

   541    arguments and is used as a predicate. *)

   542 fun is_predicate NONE s =

   543     s = "equal" orelse String.isPrefix type_const_prefix s orelse

   544     String.isPrefix class_prefix s

   545   | is_predicate (SOME the_const_tab) s =

   546     case Symtab.lookup the_const_tab s of

   547       SOME {min_arity, max_arity, sub_level} =>

   548       not sub_level andalso min_arity = max_arity

   549     | NONE => false

   551 fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =

   552   if s = type_wrapper_name then

   553     case ts of

   554       [_, t' as ATerm ((s', _), _)] =>

   555       if is_predicate const_tab s' then t' else boolify t

   556     | _ => raise Fail "malformed type wrapper"

   557   else

   558     t |> not (is_predicate const_tab s) ? boolify

   560 fun close_universally phi =

   561   let

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

   563         (is_tptp_variable s andalso not (member (op =) bounds name))

   564           ? insert (op =) name

   565         #> fold (term_vars bounds) tms

   566     fun formula_vars bounds (AQuant (q, xs, phi)) =

   567         formula_vars (xs @ bounds) phi

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

   569       | formula_vars bounds (AAtom tm) = term_vars bounds tm

   570   in

   571     case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)

   572   end

   574 fun repair_formula thy explicit_forall full_types const_tab =

   575   let

   576     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)

   577       | aux (AConn (c, phis)) = AConn (c, map aux phis)

   578       | aux (AAtom tm) =

   579         AAtom (tm |> repair_applications_in_term thy full_types const_tab

   580                   |> repair_predicates_in_term const_tab)

   581   in aux #> explicit_forall ? close_universally end

   583 fun repair_problem_line thy explicit_forall full_types const_tab

   584                         (Fof (ident, kind, phi)) =

   585   Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)

   586 fun repair_problem_with_const_table thy =

   587   map o apsnd o map ooo repair_problem_line thy

   589 fun repair_problem thy explicit_forall full_types explicit_apply problem =

   590   repair_problem_with_const_table thy explicit_forall full_types

   591       (const_table_for_problem explicit_apply problem) problem

   593 fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply

   594                     file (conjectures, axioms, helper_facts, class_rel_clauses,

   595                           arity_clauses) =

   596   let

   597     val axiom_lines = map (problem_line_for_axiom full_types) axioms

   598     val class_rel_lines =

   599       map problem_line_for_class_rel_clause class_rel_clauses

   600     val arity_lines = map problem_line_for_arity_clause arity_clauses

   601     val helper_lines = map (problem_line_for_axiom full_types) helper_facts

   602     val conjecture_lines =

   603       map (problem_line_for_conjecture full_types) conjectures

   604     val tfree_lines = problem_lines_for_free_types conjectures

   605     (* Reordering these might or might not confuse the proof reconstruction

   606        code or the SPASS Flotter hack. *)

   607     val problem =

   608       [("Relevant facts", axiom_lines),

   609        ("Class relationships", class_rel_lines),

   610        ("Arity declarations", arity_lines),

   611        ("Helper facts", helper_lines),

   612        ("Conjectures", conjecture_lines),

   613        ("Type variables", tfree_lines)]

   614       |> repair_problem thy explicit_forall full_types explicit_apply

   615     val (problem, pool) = nice_tptp_problem readable_names problem

   616     val conjecture_offset =

   617       length axiom_lines + length class_rel_lines + length arity_lines

   618       + length helper_lines

   619     val _ = File.write_list file (strings_for_tptp_problem problem)

   620   in

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

   622      conjecture_offset)

   623   end

   625 fun extract_clause_sequence output =

   626   let

   627     val tokens_of = String.tokens (not o Char.isAlphaNum)

   628     fun extract_num ("clause" :: (ss as _ :: _)) =

   629     Int.fromString (List.last ss)

   630       | extract_num _ = NONE

   631   in output |> split_lines |> map_filter (extract_num o tokens_of) end

   633 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"

   635 val parse_clause_formula_pair =

   636   $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"

   637   --| Scan.option ($$ ",")

   638 val parse_clause_formula_relation =

   639   Scan.this_string set_ClauseFormulaRelationN |-- $$ "("

   640   |-- Scan.repeat parse_clause_formula_pair

   641 val extract_clause_formula_relation =

   642   Substring.full

   643   #> Substring.position set_ClauseFormulaRelationN

   644   #> snd #> Substring.string #> strip_spaces #> explode

   645   #> parse_clause_formula_relation #> fst

   647 fun repair_conjecture_shape_and_theorem_names output conjecture_shape

   648                                               thm_names =

   649   if String.isSubstring set_ClauseFormulaRelationN output then

   650     (* This is a hack required for keeping track of axioms after they have been

   651        clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part

   652        of this hack. *)

   653     let

   654       val j0 = hd (hd conjecture_shape)

   655       val seq = extract_clause_sequence output

   656       val name_map = extract_clause_formula_relation output

   657       fun renumber_conjecture j =

   658         AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))

   659         |> map (fn s => find_index (curry (op =) s) seq + 1)

   660     in

   661       (conjecture_shape |> map (maps renumber_conjecture),

   662        seq |> map (the o AList.lookup (op =) name_map)

   663            |> map (fn s => case try (unprefix axiom_prefix) s of

   664                              SOME s' => undo_ascii_of s'

   665                            | NONE => "")

   666            |> Vector.fromList)

   667     end

   668   else

   669     (conjecture_shape, thm_names)

   672 (* generic TPTP-based provers *)

   674 fun prover_fun name

   675         {executable, required_executables, arguments, proof_delims,

   676          known_failures, max_new_relevant_facts_per_iter,

   677          prefers_theory_relevant, explicit_forall}

   678         ({debug, overlord, full_types, explicit_apply, relevance_threshold,

   679           relevance_convergence, theory_relevant, defs_relevant, isar_proof,

   680           isar_shrink_factor, ...} : params)

   681         minimize_command timeout

   682         ({subgoal, goal, relevance_override, axioms} : problem) =

   683   let

   684     val (ctxt, (_, th)) = goal;

   685     val thy = ProofContext.theory_of ctxt

   686     (* ### FIXME: (1) preprocessing for "if" etc. *)

   687     val (params, hyp_ts, concl_t) = strip_subgoal th subgoal

   688     val the_axioms =

   689       case axioms of

   690         SOME axioms => axioms

   691       | NONE => relevant_facts full_types relevance_threshold

   692                     relevance_convergence defs_relevant

   693                     max_new_relevant_facts_per_iter

   694                     (the_default prefers_theory_relevant theory_relevant)

   695                     relevance_override goal hyp_ts concl_t

   696     val (internal_thm_names, formulas) =

   697       prepare_formulas ctxt full_types hyp_ts concl_t the_axioms

   699     (* path to unique problem file *)

   700     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"

   701                        else Config.get ctxt dest_dir;

   702     val the_problem_prefix = Config.get ctxt problem_prefix;

   703     fun prob_pathname nr =

   704       let

   705         val probfile =

   706           Path.basic ((if overlord then "prob_" ^ name

   707                        else the_problem_prefix ^ serial_string ())

   708                       ^ "_" ^ string_of_int nr)

   709       in

   710         if the_dest_dir = "" then File.tmp_path probfile

   711         else if File.exists (Path.explode the_dest_dir)

   712         then Path.append (Path.explode the_dest_dir) probfile

   713         else error ("No such directory: " ^ the_dest_dir ^ ".")

   714       end;

   716     val command = Path.explode (getenv (fst executable) ^ "/" ^ snd executable)

   717     (* write out problem file and call prover *)

   718     fun command_line complete probfile =

   719       let

   720         val core = File.shell_path command ^ " " ^ arguments complete timeout ^

   721                    " " ^ File.shell_path probfile

   722       in

   723         (if Config.get ctxt measure_runtime then

   724            "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"

   725          else

   726            "exec " ^ core) ^ " 2>&1"

   727       end

   728     fun split_time s =

   729       let

   730         val split = String.tokens (fn c => str c = "\n");

   731         val (output, t) = s |> split |> split_last |> apfst cat_lines;

   732         fun as_num f = f >> (fst o read_int);

   733         val num = as_num (Scan.many1 Symbol.is_ascii_digit);

   734         val digit = Scan.one Symbol.is_ascii_digit;

   735         val num3 = as_num (digit ::: digit ::: (digit >> single));

   736         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);

   737         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;

   738       in (output, as_time t) end;

   739     fun run_on probfile =

   740       case filter (curry (op =) "" o getenv o fst)

   741                   (executable :: required_executables) of

   742         (home_var, _) :: _ =>

   743         error ("The environment variable " ^ quote home_var ^ " is not set.")

   744       | [] =>

   745         if File.exists command then

   746           let

   747             fun do_run complete =

   748               let

   749                 val command = command_line complete probfile

   750                 val ((output, msecs), res_code) =

   751                   bash_output command

   752                   |>> (if overlord then

   753                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")

   754                        else

   755                          I)

   756                   |>> (if Config.get ctxt measure_runtime then split_time

   757                        else rpair 0)

   758                 val (proof, outcome) =

   759                   extract_proof_and_outcome complete res_code proof_delims

   760                                             known_failures output

   761               in (output, msecs, proof, outcome) end

   762             val readable_names = debug andalso overlord

   763             val (pool, conjecture_offset) =

   764               write_tptp_file thy readable_names explicit_forall full_types

   765                               explicit_apply probfile formulas

   766             val conjecture_shape =

   767               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1

   768               |> map single

   769             val result =

   770               do_run false

   771               |> (fn (_, msecs0, _, SOME _) =>

   772                      do_run true

   773                      |> (fn (output, msecs, proof, outcome) =>

   774                             (output, msecs0 + msecs, proof, outcome))

   775                    | result => result)

   776           in ((pool, conjecture_shape), result) end

   777         else

   778           error ("Bad executable: " ^ Path.implode command ^ ".")

   780     (* If the problem file has not been exported, remove it; otherwise, export

   781        the proof file too. *)

   782     fun cleanup probfile =

   783       if the_dest_dir = "" then try File.rm probfile else NONE

   784     fun export probfile (_, (output, _, _, _)) =

   785       if the_dest_dir = "" then

   786         ()

   787       else

   788         File.write (Path.explode (Path.implode probfile ^ "_proof")) output

   790     val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =

   791       with_path cleanup export run_on (prob_pathname subgoal)

   792     val (conjecture_shape, internal_thm_names) =

   793       repair_conjecture_shape_and_theorem_names output conjecture_shape

   794                                                 internal_thm_names

   796     val (message, used_thm_names) =

   797       case outcome of

   798         NONE =>

   799         proof_text isar_proof

   800             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)

   801             (full_types, minimize_command, proof, internal_thm_names, th,

   802              subgoal)

   803       | SOME failure => (string_for_failure failure ^ "\n", [])

   804   in

   805     {outcome = outcome, message = message, pool = pool,

   806      used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,

   807      output = output, proof = proof, internal_thm_names = internal_thm_names,

   808      conjecture_shape = conjecture_shape}

   809   end

   811 fun get_prover_fun thy name = prover_fun name (get_prover thy name)

   813 fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n

   814                         relevance_override minimize_command proof_state name =

   815   let

   816     val thy = Proof.theory_of proof_state

   817     val birth_time = Time.now ()

   818     val death_time = Time.+ (birth_time, timeout)

   819     val prover = get_prover_fun thy name

   820     val {context = ctxt, facts, goal} = Proof.goal proof_state;

   821     val desc =

   822       "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^

   823       Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));

   824   in

   825     Async_Manager.launch das_Tool verbose birth_time death_time desc

   826         (fn () =>

   827             let

   828               val problem =

   829                 {subgoal = i, goal = (ctxt, (facts, goal)),

   830                  relevance_override = relevance_override, axioms = NONE}

   831             in

   832               prover params (minimize_command name) timeout problem |> #message

   833               handle ERROR message => "Error: " ^ message ^ "\n"

   834             end)

   835   end

   837 fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."

   838   | run_sledgehammer (params as {atps, ...}) i relevance_override

   839                      minimize_command state =

   840     case subgoal_count state of

   841       0 => priority "No subgoal!"

   842     | n =>

   843       let

   844         val _ = kill_atps ()

   845         val _ = priority "Sledgehammering..."

   846         val _ = app (start_prover_thread params i n relevance_override

   847                                          minimize_command state) atps

   848       in () end

   850 val setup =

   851   dest_dir_setup

   852   #> problem_prefix_setup

   853   #> measure_runtime_setup

   855 end;

author	blanchet
	Thu, 29 Jul 2010 16:41:32 +0200
changeset 38335	ed65a0777e10
parent 38334	a9847fb539dd
child 38337	0508ff84036f
permissions	-rw-r--r--