add support for Isar reconstruction for thf1 ATP provers like Leo-II.
authorfleury
Mon Jun 16 16:18:15 2014 +0200 (2014-06-16)
changeset 57255488046fdda59
parent 57254 d3d91422f408
child 57256 cf43583f9bb9
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
src/HOL/ATP.thy
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
     1.1 --- a/src/HOL/ATP.thy	Mon Jun 16 13:19:48 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Mon Jun 16 16:18:15 2014 +0200
     1.3 @@ -16,7 +16,6 @@
     1.4  ML_file "Tools/ATP/atp_proof.ML"
     1.5  ML_file "Tools/ATP/atp_proof_redirect.ML"
     1.6  
     1.7 -
     1.8  subsection {* Higher-order reasoning helpers *}
     1.9  
    1.10  definition fFalse :: bool where
     2.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 16 13:19:48 2014 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 16 16:18:15 2014 +0200
     2.3 @@ -44,7 +44,7 @@
     2.4  
     2.5    datatype atp_formula_role =
     2.6      Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture |
     2.7 -    Plain | Unknown
     2.8 +    Plain | Type_Role | Unknown
     2.9  
    2.10    datatype 'a atp_problem_line =
    2.11      Class_Decl of string * 'a * 'a list |
    2.12 @@ -75,9 +75,12 @@
    2.13    val tptp_exists : string
    2.14    val tptp_ho_exists : string
    2.15    val tptp_choice : string
    2.16 +  val tptp_ho_choice : string
    2.17    val tptp_not : string
    2.18    val tptp_and : string
    2.19 +  val tptp_not_and : string
    2.20    val tptp_or : string
    2.21 +  val tptp_not_or : string
    2.22    val tptp_implies : string
    2.23    val tptp_if : string
    2.24    val tptp_iff : string
    2.25 @@ -85,10 +88,13 @@
    2.26    val tptp_app : string
    2.27    val tptp_not_infix : string
    2.28    val tptp_equal : string
    2.29 +  val tptp_not_equal : string
    2.30    val tptp_old_equal : string
    2.31    val tptp_false : string
    2.32    val tptp_true : string
    2.33 +  val tptp_lambda : string
    2.34    val tptp_empty_list : string
    2.35 +  val tptp_binary_op_list : string list
    2.36    val isabelle_info_prefix : string
    2.37    val isabelle_info : string -> int -> (string, 'a) atp_term list
    2.38    val extract_isabelle_status : (string, 'a) atp_term list -> string option
    2.39 @@ -114,6 +120,9 @@
    2.40    val mk_aconn :
    2.41      atp_connective -> ('a, 'b, 'c, 'd) atp_formula
    2.42      -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula
    2.43 +  val mk_app : (string, 'a) atp_term -> (string, 'a) atp_term -> (string, 'a) atp_term
    2.44 +  val mk_apps :  (string, 'a) atp_term -> (string, 'a) atp_term list -> (string, 'a) atp_term
    2.45 +  val mk_simple_aterm:  'a -> ('a, 'b) atp_term
    2.46    val aconn_fold :
    2.47      bool option -> (bool option -> 'a -> 'b -> 'b) -> atp_connective * 'a list
    2.48      -> 'b -> 'b
    2.49 @@ -189,7 +198,7 @@
    2.50  
    2.51  datatype atp_formula_role =
    2.52    Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture |
    2.53 -  Plain | Unknown
    2.54 +  Plain | Type_Role | Unknown
    2.55  
    2.56  datatype 'a atp_problem_line =
    2.57    Class_Decl of string * 'a * 'a list |
    2.58 @@ -221,9 +230,12 @@
    2.59  val tptp_exists = "?"
    2.60  val tptp_ho_exists = "??"
    2.61  val tptp_choice = "@+"
    2.62 +val tptp_ho_choice = "@@+"
    2.63  val tptp_not = "~"
    2.64  val tptp_and = "&"
    2.65 +val tptp_not_and = "~&"
    2.66  val tptp_or = "|"
    2.67 +val tptp_not_or = "~|"
    2.68  val tptp_implies = "=>"
    2.69  val tptp_if = "<="
    2.70  val tptp_iff = "<=>"
    2.71 @@ -231,11 +243,14 @@
    2.72  val tptp_app = "@"
    2.73  val tptp_not_infix = "!"
    2.74  val tptp_equal = "="
    2.75 +val tptp_not_equal = "!="
    2.76  val tptp_old_equal = "equal"
    2.77  val tptp_false = "$false"
    2.78  val tptp_true = "$true"
    2.79 +val tptp_lambda = "^"
    2.80  val tptp_empty_list = "[]"
    2.81 -
    2.82 +val tptp_binary_op_list = [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if,
    2.83 +                             tptp_iff, tptp_not_iff, tptp_equal, tptp_app]
    2.84  val isabelle_info_prefix = "isabelle_"
    2.85  
    2.86  val inductionN = "induction"
    2.87 @@ -291,6 +306,11 @@
    2.88    | mk_anot phi = AConn (ANot, [phi])
    2.89  fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    2.90  
    2.91 +fun mk_app t u = ATerm ((tptp_app, []), [t, u])
    2.92 +fun mk_apps f xs = fold (fn x => fn f => mk_app f x) xs f
    2.93 +
    2.94 +fun mk_simple_aterm p = ATerm ((p, []), [])
    2.95 +
    2.96  fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
    2.97    | aconn_fold pos f (AImplies, [phi1, phi2]) =
    2.98      f (Option.map not pos) phi1 #> f pos phi2
    2.99 @@ -345,6 +365,7 @@
   2.100    | tptp_string_of_role Conjecture = "conjecture"
   2.101    | tptp_string_of_role Negated_Conjecture = "negated_conjecture"
   2.102    | tptp_string_of_role Plain = "plain"
   2.103 +  | tptp_string_of_role Type_Role = "type"
   2.104    | tptp_string_of_role Unknown = "unknown"
   2.105  
   2.106  fun tptp_string_of_app _ func [] = func
     3.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 16 13:19:48 2014 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 16 16:18:15 2014 +0200
     3.3 @@ -289,6 +289,8 @@
     3.4  
     3.5  val dummy_phi = AAtom (ATerm (("", []), []))
     3.6  val dummy_inference = Inference_Source ("", [])
     3.7 +val dummy_aterm = ATerm (("", []), [])
     3.8 +val dummy_atype = AType(("", []), [])
     3.9  
    3.10  (* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *)
    3.11  fun parse_dependency x =
    3.12 @@ -433,8 +435,88 @@
    3.13    | role_of_tptp_string "conjecture" = Conjecture
    3.14    | role_of_tptp_string "negated_conjecture" = Negated_Conjecture
    3.15    | role_of_tptp_string "plain" = Plain
    3.16 +  | role_of_tptp_string "type" = Type_Role
    3.17    | role_of_tptp_string _ = Unknown
    3.18  
    3.19 +fun parse_binary_op x =
    3.20 +  foldl1 (op||) (map Scan.this_string tptp_binary_op_list) x
    3.21 +
    3.22 +fun parse_thf0_type x =
    3.23 +  ($$ "(" |-- parse_thf0_type --| $$ ")"
    3.24 +   || parse_type --| $$ tptp_fun_type -- parse_thf0_type >> AFun
    3.25 +   || parse_type) x
    3.26 +
    3.27 +fun mk_ho_of_fo_quant q =
    3.28 +  if q = tptp_forall then tptp_ho_forall
    3.29 +  else if q = tptp_exists then tptp_ho_exists
    3.30 +  else raise Fail ("unrecognized quantification: " ^ q)
    3.31 +
    3.32 +fun remove_thf_app (ATerm ((x, ty), arg)) =
    3.33 +  if x = tptp_app then
    3.34 +    (case arg of
    3.35 +      ATerm ((x, ty), arg) :: t => remove_thf_app (ATerm ((x, ty), map remove_thf_app arg @ t))
    3.36 +    | [AAbs ((var, tvar), phi), t] =>
    3.37 +      remove_thf_app (AAbs ((var, tvar), map remove_thf_app phi @ [t])))
    3.38 +  else ATerm ((x, ty), map remove_thf_app arg)
    3.39 +  | remove_thf_app (AAbs (((x, ty), arg), t)) = AAbs (((x, ty), remove_thf_app arg), t)
    3.40 +
    3.41 +fun parse_thf0_typed_var x =
    3.42 +  (Scan.repeat (scan_general_id -- Scan.option ($$ ":" |-- parse_thf0_type)
    3.43 +     --| Scan.option (Scan.this_string ","))
    3.44 +   || $$ "(" |-- parse_thf0_typed_var --| $$ ")") x
    3.45 +
    3.46 +fun parse_literal_hol x =
    3.47 +  ((Scan.repeat ($$ tptp_not) >> length)
    3.48 +   -- ($$ "(" |-- parse_formula_hol_raw --| $$ ")"
    3.49 +       || scan_general_id >> mk_simple_aterm
    3.50 +       || scan_general_id --| $$ ":" --| scan_general_id >> mk_simple_aterm
    3.51 +       || (Scan.this_string tptp_ho_forall || Scan.this_string tptp_ho_exists) >> mk_simple_aterm)
    3.52 +   >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_app (mk_simple_aterm tptp_not))) x
    3.53 +
    3.54 +and parse_formula_hol_raw x =
    3.55 +  (((parse_literal_hol
    3.56 +      -- parse_binary_op
    3.57 +      -- parse_formula_hol_raw)
    3.58 +    >> (fn ((phi1, c) , phi2) =>
    3.59 +        if c = tptp_app then mk_app phi1 phi2
    3.60 +        else mk_apps (mk_simple_aterm c) [phi1, phi2]))
    3.61 +   || (Scan.this_string tptp_forall || Scan.this_string tptp_exists || Scan.this_string tptp_lambda)
    3.62 +        -- ($$ "[" |-- parse_thf0_typed_var --| $$ "]" --| $$ ":") -- parse_formula_hol_raw
    3.63 +      >> (fn ((q, t), phi) =>
    3.64 +        if q <> tptp_lambda then
    3.65 +          fold_rev
    3.66 +            (fn (var, ty) => fn r =>
    3.67 +              mk_app (q |> mk_ho_of_fo_quant |> mk_simple_aterm)
    3.68 +                (AAbs (((var, the_default dummy_atype ty), r), [])))
    3.69 +            t phi
    3.70 +        else
    3.71 +          fold_rev (fn (var, ty) => fn r => AAbs (((var, the_default dummy_atype ty), r), []))
    3.72 +                   t phi)
    3.73 +   || Scan.this_string tptp_not |-- parse_formula_hol_raw >> (mk_app (mk_simple_aterm tptp_not))
    3.74 +   || scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var, typ) => ATerm ((var, [typ]), []))
    3.75 +   || parse_literal_hol
    3.76 +   || scan_general_id >> mk_simple_aterm) x
    3.77 +
    3.78 +fun parse_formula_hol x = (parse_formula_hol_raw #>> remove_thf_app #>> AAtom) x
    3.79 +
    3.80 +fun parse_tstp_line_hol problem =
    3.81 +  ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof
    3.82 +    || Scan.this_string tptp_tff || Scan.this_string tptp_thf)
    3.83 +  -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
    3.84 +  -- parse_formula_hol -- parse_tstp_extra_arguments--| $$ ")" --| $$ "."
    3.85 +  >> (fn (((num, role), phi), deps) =>
    3.86 +      let
    3.87 +        val ((name, phi), rule, deps) =
    3.88 +          (case deps of
    3.89 +             File_Source (_, SOME s) =>
    3.90 +             (((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]), phi), "", [])
    3.91 +          | File_Source _ =>
    3.92 +             (((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
    3.93 +          | Inference_Source (rule, deps) => (((num, []), phi), rule, deps))
    3.94 +      in
    3.95 +        [(name, role_of_tptp_string role, phi, rule, map (rpair []) deps)]
    3.96 +      end)
    3.97 +
    3.98  (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
    3.99     The <num> could be an identifier, but we assume integers. *)
   3.100  fun parse_tstp_line problem =
   3.101 @@ -469,7 +551,7 @@
   3.102              [(case role_of_tptp_string role of
   3.103                 Definition =>
   3.104                 (case phi of
   3.105 -                  AAtom (ATerm (("equal", _), _)) =>
   3.106 +                 AAtom (ATerm (("equal", _), _)) =>
   3.107                    (* Vampire's equality proxy axiom *)
   3.108                    (name, Definition, phi, rule, map (rpair []) deps)
   3.109                  | _ => mk_step ())
   3.110 @@ -554,10 +636,11 @@
   3.111     >> map (core_inference z3_tptp_core_rule)) x
   3.112  
   3.113  fun parse_line name problem =
   3.114 -  if name = z3_tptpN then parse_z3_tptp_core_line
   3.115 -  else if name = spass_pirateN then  parse_spass_pirate_line
   3.116 -  else if name = spassN then  parse_spass_line
   3.117 +  if name = leo2N then parse_tstp_line_hol problem
   3.118    else if name = satallaxN then parse_satallax_core_line
   3.119 +  else if name = spassN then parse_spass_line
   3.120 +  else if name = spass_pirateN then parse_spass_pirate_line
   3.121 +  else if name = z3_tptpN then parse_z3_tptp_core_line
   3.122    else parse_tstp_line problem
   3.123  
   3.124  fun parse_proof name problem =
   3.125 @@ -573,7 +656,7 @@
   3.126      _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
   3.127    | _ => NONE)
   3.128  
   3.129 -fun atp_proof_of_tstplike_proof prover _ ""  = []
   3.130 +fun atp_proof_of_tstplike_proof prover _ "" = []
   3.131    | atp_proof_of_tstplike_proof prover problem tstp =
   3.132      (case core_of_agsyhol_proof tstp of
   3.133        SOME facts => facts |> map (core_inference agsyhol_core_rule)
     4.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jun 16 13:19:48 2014 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jun 16 16:18:15 2014 +0200
     4.3 @@ -32,9 +32,10 @@
     4.4    val exists_of : term -> term -> term
     4.5    val type_enc_aliases : (string * string list) list
     4.6    val unalias_type_enc : string -> string list
     4.7 -  val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->
     4.8 -    (string, string atp_type) atp_term -> term
     4.9 -  val prop_of_atp : Proof.context -> bool -> int Symtab.table ->
    4.10 +  val term_of_atp : Proof.context -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc ->
    4.11 +    bool -> int Symtab.table -> typ option -> (string, string atp_type) atp_term -> term
    4.12 +  val prop_of_atp : Proof.context -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc ->
    4.13 +    bool -> int Symtab.table ->
    4.14      (string, string, (string, string atp_type) atp_term, string) atp_formula -> term
    4.15  
    4.16    val used_facts_in_atp_proof :
    4.17 @@ -45,7 +46,8 @@
    4.18    val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
    4.19    val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
    4.20      ('a, 'b) atp_step
    4.21 -  val termify_atp_proof : Proof.context -> string Symtab.table -> (string * term) list ->
    4.22 +  val termify_atp_proof : Proof.context -> string -> ATP_Problem.atp_format ->
    4.23 +    ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list ->
    4.24      int Symtab.table -> string atp_proof -> (term, string) atp_step list
    4.25    val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list
    4.26    val factify_atp_proof : (string * 'a) list vector -> term list -> term ->
    4.27 @@ -140,7 +142,7 @@
    4.28    | _ => raise ATP_TERM [u])
    4.29  
    4.30  (* Accumulate type constraints in a formula: negative type literals. *)
    4.31 -fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
    4.32 +fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
    4.33  fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl)
    4.34    | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
    4.35    | add_type_constraint _ _ = I
    4.36 @@ -184,9 +186,144 @@
    4.37  val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
    4.38  val vampire_skolem_prefix = "sK"
    4.39  
    4.40 +
    4.41 +(* Higher-order translation. Variables are typed (although we don't use that information). Lambdas
    4.42 +   are typed. *)
    4.43 +fun term_of_atp_ho ctxt textual sym_tab =
    4.44 +  let
    4.45 +    val thy = Proof_Context.theory_of ctxt
    4.46 +    fun norm_var_types var T' t =
    4.47 +      let
    4.48 +        fun norm_term (ATerm ((x, ty), l)) =
    4.49 +            ATerm((x, if x = var then [T'] else ty), List.map norm_term l)
    4.50 +          | norm_term (AAbs(((x, ty), term), l)) = AAbs(((x, ty), term), List.map norm_term l)
    4.51 +      in
    4.52 +        norm_term t
    4.53 +      end
    4.54 +    fun mk_op_of_tptp_operator s =
    4.55 +      if s = tptp_or then HOLogic.mk_disj
    4.56 +      else if s = tptp_and then HOLogic.mk_conj
    4.57 +      else if s = tptp_implies then HOLogic.mk_imp
    4.58 +      else if s = tptp_iff orelse s = tptp_equal then HOLogic.mk_eq
    4.59 +      else if s = tptp_not_iff orelse s = tptp_not_equal then HOLogic.mk_eq #> HOLogic.mk_not
    4.60 +      else if s = tptp_if then HOLogic.mk_imp #> HOLogic.mk_not
    4.61 +      else if s = tptp_not_and then HOLogic.mk_conj #> HOLogic.mk_not
    4.62 +      else if s = tptp_not_or then HOLogic.mk_disj #> HOLogic.mk_not
    4.63 +      else raise Fail ("unknown operator: " ^ s)
    4.64 +    fun mk_quant_of_tptp_quant s =
    4.65 +      if s = tptp_ho_exists then HOLogic.mk_exists
    4.66 +      else if s = tptp_ho_forall then HOLogic.mk_all
    4.67 +      else raise Fail ("unknown quantifier: " ^ s)
    4.68 +    val var_index = if textual then 0 else 1
    4.69 +
    4.70 +    fun do_term opt_T u =
    4.71 +      (case u of
    4.72 +        AAbs(((var, ty), term), []) =>
    4.73 +        let val typ = typ_of_atp_type ctxt ty in
    4.74 +          absfree (repair_var_name textual var, typ) (do_term NONE (norm_var_types var ty term))
    4.75 +        end
    4.76 +      | ATerm ((s, tys), us) =>
    4.77 +        if s = ""
    4.78 +        then error "Isar proof reconstruction failed because the ATP proof \
    4.79 +                     \contains unparsable material."
    4.80 +        else if String.isPrefix native_type_prefix s then
    4.81 +          @{const True} (* ignore TPTP type information *)
    4.82 +        else if s = tptp_equal then
    4.83 +          let val ts = map (do_term NONE) us in
    4.84 +            if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then
    4.85 +              @{const True}
    4.86 +            else
    4.87 +              list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
    4.88 +          end
    4.89 +        else if s = tptp_app then
    4.90 +          let val ts = map (do_term NONE) us in
    4.91 +            hd ts $ List.last ts
    4.92 +          end
    4.93 +        else if s = tptp_not then
    4.94 +          let val ts = map (do_term NONE) us in
    4.95 +            List.last ts |> HOLogic.mk_not
    4.96 +          end
    4.97 +        else if s = tptp_ho_forall orelse s = tptp_ho_exists then
    4.98 +          (case us of
    4.99 +            [AAbs (((var, ty), term), [])] =>
   4.100 +            let val typ = typ_of_atp_type ctxt ty in
   4.101 +              (repair_var_name textual var, typ , do_term NONE (norm_var_types var ty term))
   4.102 +                |> mk_quant_of_tptp_quant s
   4.103 +            end
   4.104 +          | [] => if s = tptp_ho_exists then HOLogic.exists_const dummyT
   4.105 +                  else HOLogic.all_const dummyT)
   4.106 +        else if List.exists (curry (op=) s) tptp_binary_op_list then
   4.107 +          let val ts = map (do_term NONE) us in
   4.108 +            (mk_op_of_tptp_operator s) (hd ts, List.last ts)
   4.109 +          end
   4.110 +        else
   4.111 +          if us <> [] then
   4.112 +            let
   4.113 +              val applicant_list = List.map (do_term NONE) us
   4.114 +              val opt_typ = SOME (fold_rev
   4.115 +                                    (fn t1 => fn t2 => slack_fastype_of t1 --> t2)
   4.116 +                                    applicant_list (the_default dummyT opt_T))
   4.117 +              val func_name = do_term opt_typ (ATerm ((s, tys), []))
   4.118 +            in
   4.119 +              foldl1 (op$) (func_name :: applicant_list) end
   4.120 +          else (*FIXME: clean (remove stuff related to vampire and other provers)*)
   4.121 +            (case unprefix_and_unascii const_prefix s of
   4.122 +              SOME s' =>
   4.123 +              let
   4.124 +                val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const
   4.125 +                val new_skolem = String.isPrefix new_skolem_const_prefix s''
   4.126 +                val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s)
   4.127 +                val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
   4.128 +                val term_ts = map (do_term NONE) term_us
   4.129 +                val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us
   4.130 +                val T =
   4.131 +                    (if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then
   4.132 +                       if new_skolem then
   4.133 +                         SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
   4.134 +                       else if textual then
   4.135 +                         try (Sign.const_instance thy) (s', Ts)
   4.136 +                       else
   4.137 +                         NONE
   4.138 +                     else
   4.139 +                       NONE)
   4.140 +                       |> (fn SOME T => T
   4.141 +                            | NONE =>
   4.142 +                              map slack_fastype_of term_ts --->
   4.143 +                                the_default (Type_Infer.anyT @{sort type}) opt_T)
   4.144 +                val t =
   4.145 +                    if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
   4.146 +                    else Const (unproxify_const s', T)
   4.147 +              in list_comb (t, term_ts) end
   4.148 +            | NONE => (* a free or schematic variable *)
   4.149 +              let
   4.150 +                (* This assumes that distinct names are mapped to distinct names by
   4.151 +                   "Variable.variant_frees". This does not hold in general but should hold for
   4.152 +                   ATP-generated Skolem function names, since these end with a digit and
   4.153 +                   "variant_frees" appends letters. *)
   4.154 +                fun fresh_up s =
   4.155 +                  [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
   4.156 +                val ts = map (do_term NONE) us
   4.157 +                val T =
   4.158 +                  (case opt_T of
   4.159 +                    SOME T => map slack_fastype_of ts ---> T
   4.160 +                  | NONE =>
   4.161 +                    map slack_fastype_of ts --->
   4.162 +                      (case tys of [ty] => typ_of_atp_type ctxt ty | _ => Type_Infer.anyT
   4.163 +                        @{sort type}))
   4.164 +                val t =
   4.165 +                  (case unprefix_and_unascii fixed_var_prefix s of
   4.166 +                    SOME s => Free (s, T)
   4.167 +                  | NONE =>
   4.168 +                    if textual andalso not (is_tptp_variable s) then
   4.169 +                      Free (s |> textual ? (repair_var_name_raw #> fresh_up), T)
   4.170 +                    else
   4.171 +                      Var ((repair_var_name textual s, var_index), T))
   4.172 +              in list_comb (t, ts) end))
   4.173 +  in do_term end
   4.174 +
   4.175  (* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}"
   4.176     should allow them to be inferred. *)
   4.177 -fun term_of_atp ctxt textual sym_tab =
   4.178 +fun term_of_atp_fo ctxt textual sym_tab =
   4.179    let
   4.180      val thy = Proof_Context.theory_of ctxt
   4.181      (* For Metis, we use 1 rather than 0 because variable references in clauses may otherwise
   4.182 @@ -249,7 +386,9 @@
   4.183                    val t =
   4.184                      if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
   4.185                      else Const (unproxify_const s', T)
   4.186 -                in list_comb (t, term_ts @ extra_ts) end
   4.187 +                in
   4.188 +                  list_comb (t, term_ts @ extra_ts)
   4.189 +                end
   4.190              end
   4.191            | NONE => (* a free or schematic variable *)
   4.192              let
   4.193 @@ -283,12 +422,21 @@
   4.194              in list_comb (t, ts) end))
   4.195    in do_term [] end
   4.196  
   4.197 -fun term_of_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =
   4.198 +fun term_of_atp ctxt (ATP_Problem.THF _) type_enc =
   4.199 +    if ATP_Problem_Generate.is_type_enc_higher_order type_enc
   4.200 +    then term_of_atp_ho ctxt
   4.201 +    else error "Unsupported Isar reconstruction."
   4.202 +  | term_of_atp ctxt _ type_enc =
   4.203 +    if not (ATP_Problem_Generate.is_type_enc_higher_order type_enc)
   4.204 +    then term_of_atp_fo ctxt
   4.205 +    else error "Unsupported Isar reconstruction."
   4.206 +
   4.207 +fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) =
   4.208    if String.isPrefix class_prefix s then
   4.209      add_type_constraint pos (type_constraint_of_term ctxt u)
   4.210      #> pair @{const True}
   4.211    else
   4.212 -    pair (term_of_atp ctxt textual sym_tab (SOME @{typ bool}) u)
   4.213 +    pair (term_of_atp ctxt format type_enc textual sym_tab (SOME @{typ bool}) u)
   4.214  
   4.215  (* Update schematic type variables with detected sort constraints. It's not
   4.216     totally clear whether this code is necessary. *)
   4.217 @@ -317,7 +465,7 @@
   4.218  
   4.219  (* Interpret an ATP formula as a HOL term, extracting sort constraints as they appear in the
   4.220     formula. *)
   4.221 -fun prop_of_atp ctxt textual sym_tab phi =
   4.222 +fun prop_of_atp ctxt format type_enc textual sym_tab phi =
   4.223    let
   4.224      fun do_formula pos phi =
   4.225        (case phi of
   4.226 @@ -337,7 +485,7 @@
   4.227              | AImplies => s_imp
   4.228              | AIff => s_iff
   4.229              | ANot => raise Fail "impossible connective")
   4.230 -      | AAtom tm => term_of_atom ctxt textual sym_tab pos tm
   4.231 +      | AAtom tm => term_of_atom ctxt format type_enc textual sym_tab pos tm
   4.232        | _ => raise ATP_FORMULA [phi])
   4.233    in
   4.234      repair_tvar_sorts (do_formula true phi Vartab.empty)
   4.235 @@ -475,18 +623,19 @@
   4.236                     t
   4.237                 | t => t)
   4.238  
   4.239 -fun termify_line ctxt lifted sym_tab (name, role, u, rule, deps) =
   4.240 -  let
   4.241 -    val thy = Proof_Context.theory_of ctxt
   4.242 -    val t = u
   4.243 -      |> prop_of_atp ctxt true sym_tab
   4.244 -      |> uncombine_term thy
   4.245 -      |> unlift_term lifted
   4.246 -      |> infer_formula_types ctxt
   4.247 -      |> HOLogic.mk_Trueprop
   4.248 -  in
   4.249 -    (name, role, t, rule, deps)
   4.250 -  end
   4.251 +fun termify_line _ _ _ _ _ (_, Type_Role, _, _, _) =  NONE
   4.252 +  | termify_line ctxt format type_enc lifted sym_tab (name, role, u, rule, deps) =
   4.253 +    let
   4.254 +      val thy = Proof_Context.theory_of ctxt
   4.255 +      val t = u
   4.256 +        |> prop_of_atp ctxt format type_enc true sym_tab
   4.257 +        |> uncombine_term thy
   4.258 +        |> unlift_term lifted
   4.259 +        |> infer_formula_types ctxt
   4.260 +        |> HOLogic.mk_Trueprop
   4.261 +    in
   4.262 +      SOME (name, role, t, rule, deps)
   4.263 +    end
   4.264  
   4.265  val waldmeister_conjecture_num = "1.0.0.0"
   4.266  
   4.267 @@ -502,12 +651,12 @@
   4.268      repair_body proof
   4.269    end
   4.270  
   4.271 -fun termify_atp_proof ctxt pool lifted sym_tab =
   4.272 +fun termify_atp_proof ctxt prover format type_enc pool lifted sym_tab =
   4.273    clean_up_atp_proof_dependencies
   4.274    #> nasty_atp_proof pool
   4.275    #> map_term_names_in_atp_proof repair_name
   4.276 -  #> map (termify_line ctxt lifted sym_tab)
   4.277 -  #> repair_waldmeister_endgame
   4.278 +  #> map_filter (termify_line ctxt format type_enc lifted sym_tab)
   4.279 +  #> prover = waldmeisterN ? repair_waldmeister_endgame
   4.280  
   4.281  fun take_distinct_vars seen ((t as Var _) :: ts) =
   4.282      if member (op aconv) seen t then rev seen else take_distinct_vars (t :: seen) ts
     5.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 16 13:19:48 2014 +0200
     5.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 16 16:18:15 2014 +0200
     5.3 @@ -569,7 +569,6 @@
     5.4  
     5.5  val vampire = (vampireN, fn () => vampire_config)
     5.6  
     5.7 -
     5.8  (* Z3 with TPTP syntax (half experimental, half legacy) *)
     5.9  
    5.10  val z3_tff0 = TFF Monomorphic
    5.11 @@ -796,7 +795,7 @@
    5.12  
    5.13  val atps =
    5.14    [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
    5.15 -   z3_tptp,zipperposition, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof,
    5.16 +   z3_tptp, zipperposition, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof,
    5.17     remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
    5.18     remote_spass_pirate, remote_waldmeister]
    5.19  
     6.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 16 13:19:48 2014 +0200
     6.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 16 16:18:15 2014 +0200
     6.3 @@ -48,7 +48,7 @@
     6.4      ATerm ((Metis_Name.toString s, []), [])
     6.5  
     6.6  fun hol_term_of_metis ctxt type_enc sym_tab =
     6.7 -  atp_term_of_metis type_enc #> term_of_atp ctxt false sym_tab NONE
     6.8 +  atp_term_of_metis type_enc #> term_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab NONE
     6.9  
    6.10  fun atp_literal_of_metis type_enc (pos, atom) =
    6.11    atom |> Metis_Term.Fn |> atp_term_of_metis type_enc
    6.12 @@ -65,7 +65,7 @@
    6.13    Metis_Thm.clause
    6.14    #> Metis_LiteralSet.toList
    6.15    #> atp_clause_of_metis type_enc
    6.16 -  #> prop_of_atp ctxt false sym_tab
    6.17 +  #> prop_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab
    6.18    #> singleton (polish_hol_terms ctxt concealed)
    6.19  
    6.20  fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms =
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jun 16 13:19:48 2014 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jun 16 16:18:15 2014 +0200
     7.3 @@ -302,36 +302,39 @@
     7.4                  | NONE => NONE)
     7.5                | _ => outcome)
     7.6            in
     7.7 -            ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
     7.8 +            ((SOME key, value), (output, run_time, facts, atp_proof, outcome),
     7.9 +              SOME (format, type_enc))
    7.10            end
    7.11  
    7.12          val timer = Timer.startRealTimer ()
    7.13  
    7.14 -        fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _))) =
    7.15 +        fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) =
    7.16              let val time_left = Time.- (timeout, Timer.checkRealTimer timer) in
    7.17                if Time.<= (time_left, Time.zeroTime) then
    7.18                  result
    7.19                else
    7.20                  run_slice time_left cache slice
    7.21 -                |> (fn (cache, (output, run_time, used_from, atp_proof, outcome)) =>
    7.22 -                  (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome)))
    7.23 +                |> (fn (cache, (output, run_time, used_from, atp_proof, outcome),
    7.24 +                        format_type_enc) =>
    7.25 +                  (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome),
    7.26 +                   format_type_enc))
    7.27              end
    7.28            | maybe_run_slice _ result = result
    7.29        in
    7.30          ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
    7.31 -         ("", Time.zeroTime, [], [], SOME InternalError))
    7.32 +         ("", Time.zeroTime, [], [], SOME InternalError), NONE)
    7.33          |> fold maybe_run_slice actual_slices
    7.34        end
    7.35  
    7.36      (* If the problem file has not been exported, remove it; otherwise, export
    7.37         the proof file too. *)
    7.38      fun clean_up () = if dest_dir = "" then (try File.rm prob_path; ()) else ()
    7.39 -    fun export (_, (output, _, _, _, _)) =
    7.40 +    fun export (_, (output, _, _, _, _), _) =
    7.41        if dest_dir = "" then ()
    7.42        else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
    7.43  
    7.44      val ((_, (_, pool, fact_names, lifted, sym_tab)),
    7.45 -         (output, run_time, used_from, atp_proof, outcome)) =
    7.46 +         (output, run_time, used_from, atp_proof, outcome), SOME (format, type_enc)) =
    7.47        with_cleanup clean_up run () |> tap export
    7.48  
    7.49      val important_message =
    7.50 @@ -367,7 +370,7 @@
    7.51                        if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE
    7.52                      val atp_proof =
    7.53                        atp_proof
    7.54 -                      |> termify_atp_proof ctxt pool lifted sym_tab
    7.55 +                      |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab
    7.56                        |> introduce_spass_skolem
    7.57                        |> factify_atp_proof fact_names hyp_ts concl_t
    7.58                    in