first step towards polymorphic TFF + changed defaults for Vampire
authorblanchet
Tue Aug 30 16:07:34 2011 +0200 (2011-08-30)
changeset 445890a1dfc6365e9
parent 44588 e74aa9d9162b
child 44590 3a8a31be92d2
first step towards polymorphic TFF + changed defaults for Vampire
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:04:23 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:07:34 2011 +0200
     1.3 @@ -19,14 +19,15 @@
     1.4  
     1.5    datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
     1.6  
     1.7 -  datatype tff_flavor = Implicit | Explicit
     1.8 -  datatype thf_flavor = Without_Choice | With_Choice
     1.9 +  datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
    1.10 +  datatype tff_explicitness = TFF_Implicit | TFF_Explicit
    1.11 +  datatype thf_flavor = THF_Without_Choice | THF_With_Choice
    1.12    datatype format =
    1.13      CNF |
    1.14      CNF_UEQ |
    1.15      FOF |
    1.16 -    TFF of tff_flavor |
    1.17 -    THF of thf_flavor
    1.18 +    TFF of tff_polymorphism * tff_explicitness |
    1.19 +    THF0 of thf_flavor
    1.20  
    1.21    datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    1.22    datatype 'a problem_line =
    1.23 @@ -119,15 +120,16 @@
    1.24  
    1.25  datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
    1.26  
    1.27 -datatype tff_flavor = Implicit | Explicit
    1.28 -datatype thf_flavor = Without_Choice | With_Choice
    1.29 +datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
    1.30 +datatype tff_explicitness = TFF_Implicit | TFF_Explicit
    1.31 +datatype thf_flavor = THF_Without_Choice | THF_With_Choice
    1.32  
    1.33  datatype format =
    1.34    CNF |
    1.35    CNF_UEQ |
    1.36    FOF |
    1.37 -  TFF of tff_flavor |
    1.38 -  THF of thf_flavor
    1.39 +  TFF of tff_polymorphism * tff_explicitness |
    1.40 +  THF0 of thf_flavor
    1.41  
    1.42  datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    1.43  datatype 'a problem_line =
    1.44 @@ -211,10 +213,10 @@
    1.45    | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
    1.46    | formula_map f (AAtom tm) = AAtom (f tm)
    1.47  
    1.48 -fun is_format_thf (THF _) = true
    1.49 +fun is_format_thf (THF0 _) = true
    1.50    | is_format_thf _ = false
    1.51  fun is_format_typed (TFF _) = true
    1.52 -  | is_format_typed (THF _) = true
    1.53 +  | is_format_typed (THF0 _) = true
    1.54    | is_format_typed _ = false
    1.55  
    1.56  fun string_for_kind Axiom = "axiom"
    1.57 @@ -228,7 +230,7 @@
    1.58      raise Fail "unexpected higher-order type in first-order format"
    1.59    | strip_tff_type (AType s) = ([], s)
    1.60  
    1.61 -fun string_for_type (THF _) ty =
    1.62 +fun string_for_type (THF0 _) ty =
    1.63      let
    1.64        fun aux _ (AType s) = s
    1.65          | aux rhs (AFun (ty1, ty2)) =
    1.66 @@ -270,7 +272,7 @@
    1.67        |> is_format_thf format ? enclose "(" ")"
    1.68      else
    1.69        (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
    1.70 -             s = tptp_choice andalso format = THF With_Choice, ts) of
    1.71 +             s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of
    1.72           (true, _, [AAbs ((s', ty), tm)]) =>
    1.73           (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
    1.74              possible, to work around LEO-II 1.2.8 parser limitation. *)
    1.75 @@ -291,7 +293,7 @@
    1.76             else
    1.77               s ^ "(" ^ commas ss ^ ")"
    1.78           end)
    1.79 -  | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
    1.80 +  | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
    1.81      "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
    1.82      string_for_term format tm ^ ")"
    1.83    | string_for_term _ _ = raise Fail "unexpected term in first-order format"
    1.84 @@ -324,7 +326,7 @@
    1.85    | string_for_format CNF_UEQ = tptp_cnf
    1.86    | string_for_format FOF = tptp_fof
    1.87    | string_for_format (TFF _) = tptp_tff
    1.88 -  | string_for_format (THF _) = tptp_thf
    1.89 +  | string_for_format (THF0 _) = tptp_thf
    1.90  
    1.91  fun string_for_problem_line format (Decl (ident, sym, ty)) =
    1.92      string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:04:23 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:07:34 2011 +0200
     2.3 @@ -241,8 +241,8 @@
     2.4     prem_kind = Hypothesis,
     2.5     best_slices = fn ctxt =>
     2.6       (* FUDGE *)
     2.7 -     [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))),
     2.8 -      (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))]
     2.9 +     [(0.667, (false, (150, THF0 THF_Without_Choice, "simple_higher", sosN))),
    2.10 +      (0.333, (true, (50, THF0 THF_Without_Choice, "simple_higher", no_sosN)))]
    2.11       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    2.12           else I)}
    2.13  
    2.14 @@ -262,7 +262,8 @@
    2.15     conj_sym_kind = Axiom,
    2.16     prem_kind = Hypothesis,
    2.17     best_slices =
    2.18 -     K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)}
    2.19 +     K [(1.0, (true, (100, THF0 THF_With_Choice, "simple_higher", "")))]
    2.20 +     (* FUDGE *)}
    2.21  
    2.22  val satallax = (satallaxN, satallax_config)
    2.23  
    2.24 @@ -309,6 +310,8 @@
    2.25  fun is_old_vampire_version () =
    2.26    string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
    2.27  
    2.28 +val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit)
    2.29 +
    2.30  val vampire_config : atp_config =
    2.31    {exec = ("VAMPIRE_HOME", "vampire"),
    2.32     required_execs = [],
    2.33 @@ -340,9 +343,9 @@
    2.34           (0.333, (false, (500, FOF, "mono_tags?", sosN))),
    2.35           (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
    2.36        else
    2.37 -        [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))),
    2.38 -         (0.333, (false, (500, TFF Implicit, "simple", sosN))),
    2.39 -         (0.334, (true, (50, TFF Implicit, "simple", no_sosN)))])
    2.40 +        [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
    2.41 +         (0.333, (false, (500, vampire_tff, "simple", sosN))),
    2.42 +         (0.334, (true, (50, vampire_tff, "simple", no_sosN)))])
    2.43       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    2.44           else I)}
    2.45  
    2.46 @@ -351,6 +354,8 @@
    2.47  
    2.48  (* Z3 with TPTP syntax *)
    2.49  
    2.50 +val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit)
    2.51 +
    2.52  val z3_tptp_config : atp_config =
    2.53    {exec = ("Z3_HOME", "z3"),
    2.54     required_execs = [],
    2.55 @@ -368,10 +373,10 @@
    2.56     prem_kind = Hypothesis,
    2.57     best_slices =
    2.58       (* FUDGE *)
    2.59 -     K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
    2.60 -        (0.25, (false, (125, FOF, "mono_guards?", ""))),
    2.61 -        (0.125, (false, (62, TFF Implicit, "simple", ""))),
    2.62 -        (0.125, (false, (31, TFF Implicit, "simple", "")))]}
    2.63 +     K [(0.5, (false, (250, z3_tff, "simple", ""))),
    2.64 +        (0.25, (false, (125, z3_tff, "simple", ""))),
    2.65 +        (0.125, (false, (62, z3_tff, "simple", ""))),
    2.66 +        (0.125, (false, (31, z3_tff, "simple", "")))]}
    2.67  
    2.68  val z3_tptp = (z3_tptpN, z3_tptp_config)
    2.69  
    2.70 @@ -381,7 +386,8 @@
    2.71  val systems = Synchronized.var "atp_systems" ([] : string list)
    2.72  
    2.73  fun get_systems () =
    2.74 -  case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
    2.75 +  case Isabelle_System.bash_output
    2.76 +           "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
    2.77      (output, 0) => split_lines output
    2.78    | (output, _) =>
    2.79      error (case extract_known_failure known_perl_failures output of
    2.80 @@ -449,31 +455,32 @@
    2.81    (remote_prefix ^ name,
    2.82     remotify_config system_name system_versions best_slice config)
    2.83  
    2.84 +val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit)
    2.85 +
    2.86  val remote_e =
    2.87    remotify_atp e "EP" ["1.0", "1.1", "1.2"]
    2.88                 (K (750, FOF, "mono_tags?") (* FUDGE *))
    2.89  val remote_leo2 =
    2.90    remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
    2.91 -               (K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
    2.92 +               (K (100, THF0 THF_Without_Choice, "simple_higher") (* FUDGE *))
    2.93  val remote_satallax =
    2.94    remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
    2.95 -               (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
    2.96 +               (K (100, THF0 THF_With_Choice, "simple_higher") (* FUDGE *))
    2.97  val remote_vampire =
    2.98    remotify_atp vampire "Vampire" ["1.8"]
    2.99 -               (K (250, TFF Implicit, "simple") (* FUDGE *))
   2.100 +               (K (250, FOF, "mono_guards?") (* FUDGE *))
   2.101  val remote_z3_tptp =
   2.102 -  remotify_atp z3_tptp "Z3" ["3.0"]
   2.103 -                       (K (250, TFF Implicit, "simple") (* FUDGE *))
   2.104 +  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "simple") (* FUDGE *))
   2.105  val remote_e_sine =
   2.106    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
   2.107               Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
   2.108  val remote_snark =
   2.109    remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
   2.110               [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
   2.111 -             (K (100, TFF Explicit, "simple") (* FUDGE *))
   2.112 +             (K (100, dumb_tff, "simple") (* FUDGE *))
   2.113  val remote_e_tofof =
   2.114 -  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
   2.115 -             Axiom Hypothesis (K (150, TFF Explicit, "simple") (* FUDGE *))
   2.116 +  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
   2.117 +             Hypothesis (K (150, dumb_tff, "simple") (* FUDGE *))
   2.118  val remote_waldmeister =
   2.119    remote_atp waldmeisterN "Waldmeister" ["710"]
   2.120               [("#START OF PROOF", "Proved Goals:")]
     3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:04:23 2011 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:34 2011 +0200
     3.3 @@ -320,7 +320,7 @@
     3.4    fun default c = const_prefix ^ lookup_const c
     3.5  in
     3.6    fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
     3.7 -    | make_fixed_const (SOME (THF With_Choice)) c =
     3.8 +    | make_fixed_const (SOME (THF0 THF_With_Choice)) c =
     3.9          if c = choice_const then tptp_choice else default c
    3.10      | make_fixed_const _ c = default c
    3.11  end
    3.12 @@ -625,7 +625,7 @@
    3.13    | is_type_level_monotonicity_based Fin_Nonmono_Types = true
    3.14    | is_type_level_monotonicity_based _ = false
    3.15  
    3.16 -fun adjust_type_enc (THF _) type_enc = type_enc
    3.17 +fun adjust_type_enc (THF0 _) type_enc = type_enc
    3.18    | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
    3.19      Simple_Types (First_Order, level)
    3.20    | adjust_type_enc format (Simple_Types (_, level)) =
    3.21 @@ -889,16 +889,17 @@
    3.22                 if is_tptp_equal s andalso length args = 2 then
    3.23                   IConst (`I tptp_equal, T, [])
    3.24                 else
    3.25 -                 (* Use a proxy even for partially applied THF equality, because
    3.26 -                    the LEO-II and Satallax parsers complain about not being
    3.27 -                    able to infer the type of "=". *)
    3.28 +                 (* Use a proxy even for partially applied THF0 equality,
    3.29 +                    because the LEO-II and Satallax parsers complain about not
    3.30 +                    being able to infer the type of "=". *)
    3.31                   IConst (proxy_base |>> prefix const_prefix, T, T_args)
    3.32               | _ => IConst (name, T, [])
    3.33             else
    3.34               IConst (proxy_base |>> prefix const_prefix, T, T_args)
    3.35            | NONE => if s = tptp_choice then
    3.36                        tweak_ho_quant tptp_choice T args
    3.37 -                    else IConst (name, T, T_args))
    3.38 +                    else
    3.39 +                      IConst (name, T, T_args))
    3.40        | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
    3.41        | intro _ _ tm = tm
    3.42    in intro true [] end
    3.43 @@ -2177,12 +2178,10 @@
    3.44        |> (case format of
    3.45              CNF => ensure_cnf_problem
    3.46            | CNF_UEQ => filter_cnf_ueq_problem
    3.47 -          | _ => I)
    3.48 -      |> (if is_format_typed format andalso format <> TFF Implicit then
    3.49 -            declare_undeclared_syms_in_atp_problem type_decl_prefix
    3.50 -                                                   implicit_declsN
    3.51 -          else
    3.52 -            I)
    3.53 +          | FOF => I
    3.54 +          | TFF (_, TFF_Implicit) => I
    3.55 +          | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
    3.56 +                                                        implicit_declsN)
    3.57      val (problem, pool) = problem |> nice_atp_problem readable_names
    3.58      val helpers_offset = offset_of_heading_in_problem helpersN problem 0
    3.59      val typed_helpers =