distinguish THF syntax with and without choice (Satallax vs. LEO-II)
authorblanchet
Wed Aug 17 10:03:58 2011 +0200 (2011-08-17)
changeset 4423585e9dad3c187
parent 44234 17ae4af434aa
child 44236 b73b7832b384
child 44244 567fb5f5c639
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
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 16 15:02:20 2011 -0700
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Aug 17 10:03:58 2011 +0200
     1.3 @@ -19,7 +19,14 @@
     1.4  
     1.5    datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
     1.6  
     1.7 -  datatype format = CNF | CNF_UEQ | FOF | TFF | THF
     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 +    THF of thf_flavor
    1.15 +
    1.16    datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    1.17    datatype 'a problem_line =
    1.18      Decl of string * 'a * 'a ho_type |
    1.19 @@ -73,6 +80,7 @@
    1.20      bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
    1.21      -> 'd -> 'd
    1.22    val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
    1.23 +  val is_format_thf : format -> bool
    1.24    val is_format_typed : format -> bool
    1.25    val tptp_lines_for_atp_problem : format -> string problem -> string list
    1.26    val ensure_cnf_problem :
    1.27 @@ -107,7 +115,14 @@
    1.28  
    1.29  datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
    1.30  
    1.31 -datatype format = CNF | CNF_UEQ | FOF | TFF | THF
    1.32 +datatype thf_flavor = Without_Choice | With_Choice
    1.33 +datatype format =
    1.34 +  CNF |
    1.35 +  CNF_UEQ |
    1.36 +  FOF |
    1.37 +  TFF |
    1.38 +  THF of thf_flavor
    1.39 +
    1.40  datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    1.41  datatype 'a problem_line =
    1.42    Decl of string * 'a * 'a ho_type |
    1.43 @@ -189,7 +204,11 @@
    1.44    | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
    1.45    | formula_map f (AAtom tm) = AAtom (f tm)
    1.46  
    1.47 -val is_format_typed = member (op =) [TFF, THF]
    1.48 +fun is_format_thf (THF _) = true
    1.49 +  | is_format_thf _ = false
    1.50 +fun is_format_typed TFF = true
    1.51 +  | is_format_typed (THF _) = true
    1.52 +  | is_format_typed _ = false
    1.53  
    1.54  fun string_for_kind Axiom = "axiom"
    1.55    | string_for_kind Definition = "definition"
    1.56 @@ -202,7 +221,7 @@
    1.57      raise Fail "unexpected higher-order type in first-order format"
    1.58    | strip_tff_type (AType s) = ([], s)
    1.59  
    1.60 -fun string_for_type THF ty =
    1.61 +fun string_for_type (THF _) ty =
    1.62      let
    1.63        fun aux _ (AType s) = s
    1.64          | aux rhs (AFun (ty1, ty2)) =
    1.65 @@ -228,7 +247,7 @@
    1.66    | string_for_connective AIff = tptp_iff
    1.67  
    1.68  fun string_for_bound_var format (s, ty) =
    1.69 -  s ^ (if format = TFF orelse format = THF then
    1.70 +  s ^ (if is_format_typed format then
    1.71           " " ^ tptp_has_type ^ " " ^
    1.72           string_for_type format (ty |> the_default (AType tptp_individual_type))
    1.73         else
    1.74 @@ -241,7 +260,7 @@
    1.75        "[" ^ commas (map (string_for_term format) ts) ^ "]"
    1.76      else if is_tptp_equal s then
    1.77        space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
    1.78 -      |> format = THF ? enclose "(" ")"
    1.79 +      |> is_format_thf format ? enclose "(" ")"
    1.80      else
    1.81        (case (s = tptp_ho_forall orelse s = tptp_ho_exists, ts) of
    1.82           (true, [AAbs ((s', ty), tm)]) =>
    1.83 @@ -252,14 +271,14 @@
    1.84                        [(s', SOME ty)], AAtom tm))
    1.85         | _ =>
    1.86           let val ss = map (string_for_term format) ts in
    1.87 -           if format = THF then
    1.88 +           if is_format_thf format then
    1.89               "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
    1.90             else
    1.91               s ^ "(" ^ commas ss ^ ")"
    1.92           end)
    1.93 -  | string_for_term THF (AAbs ((s, ty), tm)) =
    1.94 -    "(^[" ^ s ^ " : " ^ string_for_type THF ty ^ "] : " ^
    1.95 -    string_for_term THF tm ^ ")"
    1.96 +  | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
    1.97 +    "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
    1.98 +    string_for_term format tm ^ ")"
    1.99    | string_for_term _ _ = raise Fail "unexpected term in first-order format"
   1.100  and string_for_formula format (AQuant (q, xs, phi)) =
   1.101      string_for_quantifier q ^
   1.102 @@ -270,10 +289,10 @@
   1.103          (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) =
   1.104      space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
   1.105                    (map (string_for_term format) ts)
   1.106 -    |> format = THF ? enclose "(" ")"
   1.107 +    |> is_format_thf format ? enclose "(" ")"
   1.108    | string_for_formula format (AConn (c, [phi])) =
   1.109      string_for_connective c ^ " " ^
   1.110 -    (string_for_formula format phi |> format = THF ? enclose "(" ")")
   1.111 +    (string_for_formula format phi |> is_format_thf format ? enclose "(" ")")
   1.112      |> enclose "(" ")"
   1.113    | string_for_formula format (AConn (c, phis)) =
   1.114      space_implode (" " ^ string_for_connective c ^ " ")
   1.115 @@ -290,7 +309,7 @@
   1.116    | string_for_format CNF_UEQ = tptp_cnf
   1.117    | string_for_format FOF = tptp_fof
   1.118    | string_for_format TFF = tptp_tff
   1.119 -  | string_for_format THF = tptp_thf
   1.120 +  | string_for_format (THF _) = tptp_thf
   1.121  
   1.122  fun string_for_problem_line format (Decl (ident, sym, ty)) =
   1.123      string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 16 15:02:20 2011 -0700
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 17 10:03:58 2011 +0200
     2.3 @@ -242,7 +242,7 @@
     2.4     known_failures = [],
     2.5     conj_sym_kind = Axiom,
     2.6     prem_kind = Hypothesis,
     2.7 -   formats = [THF, FOF],
     2.8 +   formats = [THF Without_Choice, FOF],
     2.9     best_slices = fn ctxt =>
    2.10       (* FUDGE *)
    2.11       [(0.667, (false, (150, "simple_higher", sosN))),
    2.12 @@ -265,7 +265,7 @@
    2.13     known_failures = [(ProofMissing, "SZS status Theorem")],
    2.14     conj_sym_kind = Axiom,
    2.15     prem_kind = Hypothesis,
    2.16 -   formats = [THF],
    2.17 +   formats = [THF With_Choice],
    2.18     best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
    2.19  
    2.20  val satallax = (satallaxN, satallax_config)
     3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 16 15:02:20 2011 -0700
     3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 17 10:03:58 2011 +0200
     3.3 @@ -604,12 +604,14 @@
     3.4  val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
     3.5  
     3.6  fun choose_format formats (Simple_Types (order, level)) =
     3.7 -    if member (op =) formats THF then
     3.8 -      (THF, Simple_Types (order, level))
     3.9 -    else if member (op =) formats TFF then
    3.10 -      (TFF, Simple_Types (First_Order, level))
    3.11 -    else
    3.12 -      choose_format formats (Guards (Mangled_Monomorphic, level, Heavyweight))
    3.13 +    (case find_first is_format_thf formats of
    3.14 +       SOME format => (format, Simple_Types (order, level))
    3.15 +     | NONE =>
    3.16 +       if member (op =) formats TFF then
    3.17 +         (TFF, Simple_Types (First_Order, level))
    3.18 +       else
    3.19 +         choose_format formats
    3.20 +                       (Guards (Mangled_Monomorphic, level, Heavyweight)))
    3.21    | choose_format formats type_enc =
    3.22      (case hd formats of
    3.23         CNF_UEQ =>
    3.24 @@ -760,7 +762,7 @@
    3.25                 (true, @{type_name bool}) => `I tptp_bool_type
    3.26               | (true, @{type_name fun}) => `I tptp_fun_type
    3.27               | _ => if s = homo_infinite_type_name andalso
    3.28 -                       (format = TFF orelse format = THF) then
    3.29 +                       is_format_typed format then
    3.30                        `I tptp_individual_type
    3.31                      else
    3.32                        `make_fixed_type_const s,