make TFF output less explicit where possible
authorblanchet
Thu Aug 25 22:05:18 2011 +0200 (2011-08-25)
changeset 444998870232a87ad
parent 44498 a4cbf5668a54
child 44500 dbd98b549597
make TFF output less explicit where possible
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	Thu Aug 25 19:09:39 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 25 22:05:18 2011 +0200
     1.3 @@ -19,12 +19,13 @@
     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 format =
    1.10      CNF |
    1.11      CNF_UEQ |
    1.12      FOF |
    1.13 -    TFF |
    1.14 +    TFF of tff_flavor |
    1.15      THF of thf_flavor
    1.16  
    1.17    datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    1.18 @@ -118,12 +119,14 @@
    1.19  
    1.20  datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
    1.21  
    1.22 +datatype tff_flavor = Implicit | Explicit
    1.23  datatype thf_flavor = Without_Choice | With_Choice
    1.24 +
    1.25  datatype format =
    1.26    CNF |
    1.27    CNF_UEQ |
    1.28    FOF |
    1.29 -  TFF |
    1.30 +  TFF of tff_flavor |
    1.31    THF of thf_flavor
    1.32  
    1.33  datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    1.34 @@ -210,7 +213,7 @@
    1.35  
    1.36  fun is_format_thf (THF _) = true
    1.37    | is_format_thf _ = false
    1.38 -fun is_format_typed TFF = true
    1.39 +fun is_format_typed (TFF _) = true
    1.40    | is_format_typed (THF _) = true
    1.41    | is_format_typed _ = false
    1.42  
    1.43 @@ -232,7 +235,7 @@
    1.44            aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2
    1.45            |> not rhs ? enclose "(" ")"
    1.46      in aux true ty end
    1.47 -  | string_for_type TFF ty =
    1.48 +  | string_for_type (TFF _) ty =
    1.49      (case strip_tff_type ty of
    1.50         ([], s) => s
    1.51       | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
    1.52 @@ -320,7 +323,7 @@
    1.53  fun string_for_format CNF = tptp_cnf
    1.54    | string_for_format CNF_UEQ = tptp_cnf
    1.55    | string_for_format FOF = tptp_fof
    1.56 -  | string_for_format TFF = tptp_tff
    1.57 +  | string_for_format (TFF _) = tptp_tff
    1.58    | string_for_format (THF _) = tptp_thf
    1.59  
    1.60  fun string_for_problem_line format (Decl (ident, sym, ty)) =
     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 19:09:39 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 22:05:18 2011 +0200
     2.3 @@ -338,9 +338,9 @@
     2.4           (0.334, (true, (50, FOF, "mono_guards?", no_sosN))),
     2.5           (0.333, (false, (500, FOF, "mono_tags?", sosN)))]
     2.6        else
     2.7 -        [(0.333, (false, (150, TFF, "poly_guards", sosN))),
     2.8 -         (0.334, (true, (50, TFF, "simple", no_sosN))),
     2.9 -         (0.333, (false, (500, TFF, "simple", sosN)))])
    2.10 +        [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))),
    2.11 +         (0.334, (true, (50, TFF Implicit, "simple", no_sosN))),
    2.12 +         (0.333, (false, (500, TFF Implicit, "simple", sosN)))])
    2.13       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    2.14           else I)}
    2.15  
    2.16 @@ -368,8 +368,8 @@
    2.17       (* FUDGE *)
    2.18       K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
    2.19          (0.25, (false, (125, FOF, "mono_guards?", ""))),
    2.20 -        (0.125, (false, (62, TFF, "simple", ""))),
    2.21 -        (0.125, (false, (31, TFF, "simple", "")))]}
    2.22 +        (0.125, (false, (62, TFF Implicit, "simple", ""))),
    2.23 +        (0.125, (false, (31, TFF Implicit, "simple", "")))]}
    2.24  
    2.25  val z3_tptp = (z3_tptpN, z3_tptp_config)
    2.26  
    2.27 @@ -457,19 +457,21 @@
    2.28    remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
    2.29                 (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
    2.30  val remote_vampire =
    2.31 -  remotify_atp vampire "Vampire" ["1.8"] (K (250, TFF, "simple") (* FUDGE *))
    2.32 +  remotify_atp vampire "Vampire" ["1.8"]
    2.33 +               (K (250, TFF Implicit, "simple") (* FUDGE *))
    2.34  val remote_z3_tptp =
    2.35 -  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, TFF, "simple") (* FUDGE *))
    2.36 +  remotify_atp z3_tptp "Z3" ["3.0"]
    2.37 +                       (K (250, TFF Implicit, "simple") (* FUDGE *))
    2.38  val remote_e_sine =
    2.39    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
    2.40               Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
    2.41  val remote_snark =
    2.42    remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
    2.43               [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
    2.44 -             (K (100, TFF, "simple") (* FUDGE *))
    2.45 +             (K (100, TFF Explicit, "simple") (* FUDGE *))
    2.46  val remote_e_tofof =
    2.47    remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
    2.48 -             Axiom Hypothesis (K (150, TFF, "simple") (* FUDGE *))
    2.49 +             Axiom Hypothesis (K (150, TFF Explicit, "simple") (* FUDGE *))
    2.50  val remote_waldmeister =
    2.51    remote_atp waldmeisterN "Waldmeister" ["710"]
    2.52               [("#START OF PROOF", "Proved Goals:")]
     3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 19:09:39 2011 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 22:05:18 2011 +0200
     3.3 @@ -621,7 +621,7 @@
     3.4    | is_type_level_monotonicity_based _ = false
     3.5  
     3.6  fun adjust_type_enc (THF _) type_enc = type_enc
     3.7 -  | adjust_type_enc TFF (Simple_Types (_, level)) =
     3.8 +  | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
     3.9      Simple_Types (First_Order, level)
    3.10    | adjust_type_enc format (Simple_Types (_, level)) =
    3.11      adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))