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

     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      axiom_clauses: (string * thm) list option,

    34      filtered_clauses: (string * thm) list option}

    35   type prover_result =

    36     {outcome: failure option,

    37      message: string,

    38      pool: string Symtab.table,

    39      used_thm_names: string list,

    40      atp_run_time_in_msecs: int,

    41      output: string,

    42      proof: string,

    43      internal_thm_names: string Vector.vector,

    44      conjecture_shape: int list list,

    45      filtered_clauses: (string * thm) list}

    46   type prover =

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

    49   val dest_dir : string Config.T

    50   val problem_prefix : string Config.T

    51   val measure_runtime : bool Config.T

    52   val kill_atps: unit -> unit

    53   val running_atps: unit -> unit

    54   val messages: int option -> unit

    55   val get_prover_fun : theory -> string -> prover

    56   val run_sledgehammer :

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

    58     -> Proof.state -> unit

    59   val setup : theory -> theory

    60 end;

    62 structure Sledgehammer : SLEDGEHAMMER =

    63 struct

    65 open ATP_Problem

    66 open ATP_Systems

    67 open Metis_Clauses

    68 open Sledgehammer_Util

    69 open Sledgehammer_Fact_Filter

    70 open Sledgehammer_Proof_Reconstruct

    73 (** The Sledgehammer **)

    75 val das_Tool = "Sledgehammer"

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

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

    79 val messages = Async_Manager.thread_messages das_Tool "ATP"

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

    83 type params =

    84   {debug: bool,

    85    verbose: bool,

    86    overlord: bool,

    87    atps: string list,

    88    full_types: bool,

    89    explicit_apply: bool,

    90    relevance_threshold: real,

    91    relevance_convergence: real,

    92    theory_relevant: bool option,

    93    defs_relevant: bool,

    94    isar_proof: bool,

    95    isar_shrink_factor: int,

    96    timeout: Time.time,

    97    minimize_timeout: Time.time}

    99 type problem =

   100   {subgoal: int,

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

   102    relevance_override: relevance_override,

   103    axiom_clauses: (string * thm) list option,

   104    filtered_clauses: (string * thm) list option}

   106 type prover_result =

   107   {outcome: failure option,

   108    message: string,

   109    pool: string Symtab.table,

   110    used_thm_names: string list,

   111    atp_run_time_in_msecs: int,

   112    output: string,

   113    proof: string,

   114    internal_thm_names: string Vector.vector,

   115    conjecture_shape: int list list,

   116    filtered_clauses: (string * thm) list}

   118 type prover =

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

   121 (* configuration attributes *)

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

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

   126 val (problem_prefix, problem_prefix_setup) =

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

   129 val (measure_runtime, measure_runtime_setup) =

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

   132 fun with_path cleanup after f path =

   133   Exn.capture f path

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

   135   |> Exn.release

   136   |> tap (after path)

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

   139 fun extract_proof delims output =

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

   141                 (ListPair.unzip delims) of

   142     (SOME begin_delim, SOME end_delim) =>

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

   144             |> first_field end_delim |> the |> fst

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

   146      handle Option.Option => "")

   147   | _ => ""

   149 fun extract_proof_and_outcome complete res_code proof_delims known_failures

   150                               output =

   151   case map_filter (fn (failure, pattern) =>

   152                       if String.isSubstring pattern output then SOME failure

   153                       else NONE) known_failures of

   154     [] => (case extract_proof proof_delims output of

   155              "" => ("", SOME UnknownError)

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

   157                       else ("", SOME UnknownError))

   158   | (failure :: _) =>

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

   160                  Unprovable

   161                else

   162                  failure))

   164 fun string_for_failure Unprovable = "The ATP problem is unprovable."

   165   | string_for_failure IncompleteUnprovable =

   166     "The ATP cannot prove the problem."

   167   | string_for_failure CantConnect = "Can't connect to remote ATP."

   168   | string_for_failure TimedOut = "Timed out."

   169   | string_for_failure OutOfResources = "The ATP ran out of resources."

   170   | string_for_failure OldSpass =

   171     (* FIXME: Change the error message below to point to the Isabelle download

   172        page once the package is there. *)

   173     "Warning: Sledgehammer requires a more recent version of SPASS with \

   174     \support for the TPTP syntax. To install it, download and untar the \

   175     \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \

   176     \\"spass-3.7\" directory's full path to \"" ^

   177     Path.implode (Path.expand (Path.appends

   178         (Path.variable "ISABELLE_HOME_USER" ::

   179          map Path.basic ["etc", "components"]))) ^

   180     "\" on a line of its own."

   181   | string_for_failure MalformedInput =

   182     "Internal Sledgehammer error: The ATP problem is malformed. Please report \

   183     \this to the Isabelle developers."

   184   | string_for_failure MalformedOutput = "Error: The ATP output is malformed."

   185   | string_for_failure UnknownError = "Error: An unknown ATP error occurred."

   188 (* Clause preparation *)

   190 datatype fol_formula =

   191   FOLFormula of {formula_name: string,

   192                  kind: kind,

   193                  combformula: (name, combterm) formula,

   194                  ctypes_sorts: typ list}

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

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

   198 fun mk_ahorn [] phi = phi

   199   | mk_ahorn (phi :: phis) psi =

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

   202 (* ### FIXME: reintroduce

   203 fun make_clause_table xs =

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

   205 (* Remove existing axiom clauses from the conjecture clauses, as this can

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

   207 fun subtract_cls ax_clauses =

   208   filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)

   209 *)

   211 fun combformula_for_prop thy =

   212   let

   213     val do_term = combterm_from_term thy

   214     fun do_quant bs q s T t' =

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

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

   217     and do_conn bs c t1 t2 =

   218       do_formula bs t1 ##>> do_formula bs t2

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

   220     and do_formula bs t =

   221       case t of

   222         @{const Not} $ t1 =>

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

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

   225         do_quant bs AForall s T t'

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

   227         do_quant bs AExists s T t'

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

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

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

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

   232         do_conn bs AIff t1 t2

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

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

   235   in do_formula [] end

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

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

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

   240    "ATP_Systems".) *)

   241 (* FIXME: test! *)

   242 fun transform_elim_term t =

   243   case Logic.strip_imp_concl t of

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

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

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

   247   | _ => t

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

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

   251 fun extensionalize_term t =

   252   let

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

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

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

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

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

   258           |> aux (j + 1)

   259         end

   260       | aux _ t = t

   261   in aux (maxidx_of_term t + 1) t end

   263 (* FIXME: Guarantee freshness *)

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

   265 fun conceal_bounds Ts t =

   266   subst_bounds (map (Free o apfst concealed_bound_name)

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

   268 fun reveal_bounds Ts =

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

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

   272 fun introduce_combinators_in_term ctxt kind t =

   273   let

   274     val thy = ProofContext.theory_of ctxt

   275     fun aux Ts t =

   276       case t of

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

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

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

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

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

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

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

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

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

   286           $ t1 $ t2 =>

   287         t0 $ aux Ts t1 $ aux Ts t2

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

   289                t

   290              else

   291                let

   292                  val t = t |> conceal_bounds Ts

   293                            |> Envir.eta_contract

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

   295                in

   296                  t |> cterm_of thy

   297                    |> Clausifier.introduce_combinators_in_cterm

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

   299                    |> prop_of |> Logic.dest_equals |> snd

   300                    |> reveal_bounds Ts

   301                end

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

   303   handle THM _ =>

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

   305          case kind of

   306            Axiom => HOLogic.true_const

   307          | Conjecture => HOLogic.false_const

   309 (* making axiom and conjecture clauses *)

   310 fun make_clause ctxt (formula_name, kind, t) =

   311   let

   312     val thy = ProofContext.theory_of ctxt

   313     (* ### FIXME: perform other transformations previously done by

   314        "Clausifier.to_nnf", e.g. "HOL.If" *)

   315     val t = t |> transform_elim_term

   316               |> Object_Logic.atomize_term thy

   317               |> extensionalize_term

   318               |> introduce_combinators_in_term ctxt kind

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

   320   in

   321     FOLFormula {formula_name = formula_name, combformula = combformula,

   322                 kind = kind, ctypes_sorts = ctypes_sorts}

   323   end

   325 fun make_axiom_clause ctxt (name, th) =

   326   (name, make_clause ctxt (name, Axiom, prop_of th))

   327 fun make_conjecture_clauses ctxt ts =

   328   map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))

   329        (0 upto length ts - 1) ts

   331 (** Helper clauses **)

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

   334     Symtab.map_entry s (Integer.add 1)

   335   | count_combterm (CombVar _) = I

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

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

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

   339   | count_combformula (AAtom tm) = count_combterm tm

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

   341   count_combformula combformula

   343 val optional_helpers =

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

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

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

   347 val optional_typed_helpers =

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

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

   350 val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}

   352 val init_counters =

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

   354                     [optional_helpers, optional_typed_helpers])

   356 fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =

   357   let

   358     val ct = fold (fold count_fol_formula) [conjectures, axclauses]

   359                   init_counters

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

   361     val cnfs =

   362       (optional_helpers

   363        |> full_types ? append optional_typed_helpers

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

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

   366                    else [])) @

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

   368   in map (snd o make_axiom_clause ctxt) cnfs end

   370 fun s_not (@{const Not} $ t) = t

   371   | s_not t = @{const Not} $ t

   373 (* prepare for passing to writer,

   374    create additional clauses based on the information from extra_cls *)

   375 fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =

   376   let

   377     val thy = ProofContext.theory_of ctxt

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

   379     val is_FO = Meson.is_fol_term thy goal_t

   380     val axtms = map (prop_of o snd) extra_cls

   381     val subs = tfree_classes_of_terms [goal_t]

   382     val supers = tvar_classes_of_terms axtms

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

   384     (* TFrees in conjecture clauses; TVars in axiom clauses *)

   385     val conjectures =

   386       map (s_not o HOLogic.dest_Trueprop) hyp_ts @

   387         [HOLogic.dest_Trueprop concl_t]

   388       |> make_conjecture_clauses ctxt

   389     val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls

   390     val (clnames, axiom_clauses) =

   391       ListPair.unzip (map (make_axiom_clause ctxt) axcls)

   392     (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the

   393        "get_helper_clauses" call? *)

   394     val helper_clauses =

   395       get_helper_clauses ctxt is_FO full_types conjectures extra_clauses

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

   397     val class_rel_clauses = make_class_rel_clauses thy subs supers'

   398   in

   399     (Vector.fromList clnames,

   400       (conjectures, axiom_clauses, extra_clauses, helper_clauses,

   401        class_rel_clauses, arity_clauses))

   402   end

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

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

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

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

   409     ATerm (name, map fo_term_for_combtyp tys)

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

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

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

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

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

   418 fun fo_term_for_combterm full_types =

   419   let

   420     fun aux top_level u =

   421       let

   422         val (head, args) = strip_combterm_comb u

   423         val (x, ty_args) =

   424           case head of

   425             CombConst (name, _, ty_args) =>

   426             if fst name = "equal" then

   427               (if top_level andalso length args = 2 then name

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

   429             else

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

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

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

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

   434                           map (aux false) args)

   435     in

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

   437     end

   438   in aux true end

   440 fun formula_for_combformula full_types =

   441   let

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

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

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

   445   in aux end

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

   448   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)

   449                 (type_literals_for_types ctypes_sorts))

   450            (formula_for_combformula full_types combformula)

   452 fun problem_line_for_axiom full_types

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

   454   Fof (axiom_prefix ^ ascii_of formula_name, kind,

   455        formula_for_axiom full_types formula)

   457 fun problem_line_for_class_rel_clause

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

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

   460     Fof (ascii_of axiom_name, Axiom,

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

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

   463   end

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

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

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

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

   470 fun problem_line_for_arity_clause

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

   472   Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,

   473        mk_ahorn (map (formula_for_fo_literal o apfst not

   474                       o fo_literal_for_arity_literal) premLits)

   475                 (formula_for_fo_literal

   476                      (fo_literal_for_arity_literal conclLit)))

   478 fun problem_line_for_conjecture full_types

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

   480   Fof (conjecture_prefix ^ formula_name, kind,

   481        formula_for_combformula full_types combformula)

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

   484   map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)

   486 fun problem_line_for_free_type lit =

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

   488 fun problem_lines_for_free_types conjectures =

   489   let

   490     val litss = map free_type_literals_for_conjecture conjectures

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

   492   in map problem_line_for_free_type lits end

   494 (** "hBOOL" and "hAPP" **)

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

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

   499   (if is_tptp_variable s then

   500      I

   501    else

   502      let val n = length ts in

   503        Symtab.map_default

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

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

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

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

   508                 sub_level = sub_level orelse not top_level})

   509      end)

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

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

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

   513   | consider_formula (AAtom tm) = consider_term true tm

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

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

   518 fun const_table_for_problem explicit_apply problem =

   519   if explicit_apply then NONE

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

   522 val tc_fun = make_fixed_type_const @{type_name fun}

   524 fun min_arity_of thy full_types NONE s =

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

   526         String.isPrefix type_const_prefix s orelse

   527         String.isPrefix class_prefix s then

   528        16383 (* large number *)

   529      else if full_types then

   530        0

   531      else case strip_prefix_and_undo_ascii const_prefix s of

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

   533      | NONE => 0)

   534   | min_arity_of _ _ (SOME the_const_tab) s =

   535     case Symtab.lookup the_const_tab s of

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

   537     | NONE => 0

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

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

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

   543 fun list_hAPP_rev _ t1 [] = t1

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

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

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

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

   548                          [full_type_of t2, ty]) in

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

   550     end

   552 fun repair_applications_in_term thy full_types const_tab =

   553   let

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

   555       if s = type_wrapper_name then

   556         case ts of

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

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

   559       else

   560         let

   561           val ts = map (aux NONE) ts

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

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

   564   in aux NONE end

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

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

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

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

   571    arguments and is used as a predicate. *)

   572 fun is_predicate NONE s =

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

   574     String.isPrefix class_prefix s

   575   | is_predicate (SOME the_const_tab) s =

   576     case Symtab.lookup the_const_tab s of

   577       SOME {min_arity, max_arity, sub_level} =>

   578       not sub_level andalso min_arity = max_arity

   579     | NONE => false

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

   582   if s = type_wrapper_name then

   583     case ts of

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

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

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

   587   else

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

   590 fun close_universally phi =

   591   let

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

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

   594           ? insert (op =) name

   595         #> fold (term_vars bounds) tms

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

   597         formula_vars (xs @ bounds) phi

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

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

   600   in

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

   602   end

   604 fun repair_formula thy explicit_forall full_types const_tab =

   605   let

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

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

   608       | aux (AAtom tm) =

   609         AAtom (tm |> repair_applications_in_term thy full_types const_tab

   610                   |> repair_predicates_in_term const_tab)

   611   in aux #> explicit_forall ? close_universally end

   613 fun repair_problem_line thy explicit_forall full_types const_tab

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

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

   616 fun repair_problem_with_const_table thy =

   617   map o apsnd o map ooo repair_problem_line thy

   619 fun repair_problem thy explicit_forall full_types explicit_apply problem =

   620   repair_problem_with_const_table thy explicit_forall full_types

   621       (const_table_for_problem explicit_apply problem) problem

   623 fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply

   624                     file (conjectures, axiom_clauses, extra_clauses,

   625                           helper_clauses, class_rel_clauses, arity_clauses) =

   626   let

   627     val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses

   628     val class_rel_lines =

   629       map problem_line_for_class_rel_clause class_rel_clauses

   630     val arity_lines = map problem_line_for_arity_clause arity_clauses

   631     val helper_lines = map (problem_line_for_axiom full_types) helper_clauses

   632     val conjecture_lines =

   633       map (problem_line_for_conjecture full_types) conjectures

   634     val tfree_lines = problem_lines_for_free_types conjectures

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

   636        code or the SPASS Flotter hack. *)

   637     val problem =

   638       [("Relevant facts", axiom_lines),

   639        ("Class relationships", class_rel_lines),

   640        ("Arity declarations", arity_lines),

   641        ("Helper facts", helper_lines),

   642        ("Conjectures", conjecture_lines),

   643        ("Type variables", tfree_lines)]

   644       |> repair_problem thy explicit_forall full_types explicit_apply

   645     val (problem, pool) = nice_tptp_problem readable_names problem

   646     val conjecture_offset =

   647       length axiom_lines + length class_rel_lines + length arity_lines

   648       + length helper_lines

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

   650   in

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

   652      conjecture_offset)

   653   end

   655 fun extract_clause_sequence output =

   656   let

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

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

   659     Int.fromString (List.last ss)

   660       | extract_num _ = NONE

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

   663 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"

   665 val parse_clause_formula_pair =

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

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

   668 val parse_clause_formula_relation =

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

   670   |-- Scan.repeat parse_clause_formula_pair

   671 val extract_clause_formula_relation =

   672   Substring.full

   673   #> Substring.position set_ClauseFormulaRelationN

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

   675   #> parse_clause_formula_relation #> fst

   677 fun repair_conjecture_shape_and_theorem_names output conjecture_shape

   678                                               thm_names =

   679   if String.isSubstring set_ClauseFormulaRelationN output then

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

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

   682        of this hack. *)

   683     let

   684       val j0 = hd (hd conjecture_shape)

   685       val seq = extract_clause_sequence output

   686       val name_map = extract_clause_formula_relation output

   687       fun renumber_conjecture j =

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

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

   690     in

   691       (conjecture_shape |> map (maps renumber_conjecture),

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

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

   694                              SOME s' => undo_ascii_of s'

   695                            | NONE => "")

   696            |> Vector.fromList)

   697     end

   698   else

   699     (conjecture_shape, thm_names)

   702 (* generic TPTP-based provers *)

   704 fun prover_fun name

   705         {executable, required_executables, arguments, proof_delims,

   706          known_failures, max_new_relevant_facts_per_iter,

   707          prefers_theory_relevant, explicit_forall}

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

   709           relevance_convergence, theory_relevant, defs_relevant, isar_proof,

   710           isar_shrink_factor, ...} : params)

   711         minimize_command timeout

   712         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}

   713          : problem) =

   714   let

   715     (* get clauses and prepare them for writing *)

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

   717     val thy = ProofContext.theory_of ctxt

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

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

   720     val the_filtered_clauses =

   721       case filtered_clauses of

   722         SOME fcls => fcls

   723       | NONE => relevant_facts full_types relevance_threshold

   724                     relevance_convergence defs_relevant

   725                     max_new_relevant_facts_per_iter

   726                     (the_default prefers_theory_relevant theory_relevant)

   727                     relevance_override goal hyp_ts concl_t

   728     val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses

   729     val (internal_thm_names, clauses) =

   730       prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses

   731                       the_filtered_clauses

   733     (* path to unique problem file *)

   734     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"

   735                        else Config.get ctxt dest_dir;

   736     val the_problem_prefix = Config.get ctxt problem_prefix;

   737     fun prob_pathname nr =

   738       let

   739         val probfile =

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

   741                        else the_problem_prefix ^ serial_string ())

   742                       ^ "_" ^ string_of_int nr)

   743       in

   744         if the_dest_dir = "" then File.tmp_path probfile

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

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

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

   748       end;

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

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

   752     fun command_line complete probfile =

   753       let

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

   755                    " " ^ File.shell_path probfile

   756       in

   757         (if Config.get ctxt measure_runtime then

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

   759          else

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

   761       end

   762     fun split_time s =

   763       let

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

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

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

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

   768         val digit = Scan.one Symbol.is_ascii_digit;

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

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

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

   772       in (output, as_time t) end;

   773     fun run_on probfile =

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

   775                   (executable :: required_executables) of

   776         (home_var, _) :: _ =>

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

   778       | [] =>

   779         if File.exists command then

   780           let

   781             fun do_run complete =

   782               let

   783                 val command = command_line complete probfile

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

   785                   bash_output command

   786                   |>> (if overlord then

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

   788                        else

   789                          I)

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

   791                        else rpair 0)

   792                 val (proof, outcome) =

   793                   extract_proof_and_outcome complete res_code proof_delims

   794                                             known_failures output

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

   796             val readable_names = debug andalso overlord

   797             val (pool, conjecture_offset) =

   798               write_tptp_file thy readable_names explicit_forall full_types

   799                               explicit_apply probfile clauses

   800             val conjecture_shape =

   801               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1

   802               |> map single

   803             val result =

   804               do_run false

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

   806                      do_run true

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

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

   809                    | result => result)

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

   811         else

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

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

   815        the proof file too. *)

   816     fun cleanup probfile =

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

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

   819       if the_dest_dir = "" then

   820         ()

   821       else

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

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

   825       with_path cleanup export run_on (prob_pathname subgoal)

   826     val (conjecture_shape, internal_thm_names) =

   827       repair_conjecture_shape_and_theorem_names output conjecture_shape

   828                                                 internal_thm_names

   830     val (message, used_thm_names) =

   831       case outcome of

   832         NONE =>

   833         proof_text isar_proof

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

   835             (full_types, minimize_command, proof, internal_thm_names, th,

   836              subgoal)

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

   838   in

   839     {outcome = outcome, message = message, pool = pool,

   840      used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,

   841      output = output, proof = proof, internal_thm_names = internal_thm_names,

   842      conjecture_shape = conjecture_shape,

   843      filtered_clauses = the_filtered_clauses}

   844   end

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

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

   849                         relevance_override minimize_command proof_state name =

   850   let

   851     val thy = Proof.theory_of proof_state

   852     val birth_time = Time.now ()

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

   854     val prover = get_prover_fun thy name

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

   856     val desc =

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

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

   859   in

   860     Async_Manager.launch das_Tool verbose birth_time death_time desc

   861         (fn () =>

   862             let

   863               val problem =

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

   865                  relevance_override = relevance_override, axiom_clauses = NONE,

   866                  filtered_clauses = NONE}

   867             in

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

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

   870             end)

   871   end

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

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

   875                      minimize_command state =

   876     case subgoal_count state of

   877       0 => priority "No subgoal!"

   878     | n =>

   879       let

   880         val _ = kill_atps ()

   881         val _ = priority "Sledgehammering..."

   882         val _ = app (start_prover_thread params i n relevance_override

   883                                          minimize_command state) atps

   884       in () end

   886 val setup =

   887   dest_dir_setup

   888   #> problem_prefix_setup

   889   #> measure_runtime_setup

   891 end;

author	blanchet
	Wed, 28 Jul 2010 18:54:18 +0200
changeset 38290	463177795c49
parent 38286	174568533593
child 38307	685d1f0f75b3
permissions	-rw-r--r--