src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 37703 b4c799bab553
child 37922 ff56c361d75b
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     2
    Author:     Jia Meng, NICTA
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     4
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     5
TPTP syntax.
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     6
*)
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     7
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     8
signature SLEDGEHAMMER_TPTP_FORMAT =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     9
sig
37578
9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents: 37577
diff changeset
    10
  type classrel_clause = Metis_Clauses.classrel_clause
9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents: 37577
diff changeset
    11
  type arity_clause = Metis_Clauses.arity_clause
9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents: 37577
diff changeset
    12
  type hol_clause = Metis_Clauses.hol_clause
37624
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    13
  type name_pool = string Symtab.table * string Symtab.table
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    14
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    15
  val write_tptp_file :
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    16
    theory -> bool -> bool -> bool -> Path.T
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    17
    -> hol_clause list * hol_clause list * hol_clause list * hol_clause list
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    18
       * classrel_clause list * arity_clause list
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    19
    -> name_pool option * int
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    20
end;
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    21
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    22
structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    23
struct
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    24
37578
9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents: 37577
diff changeset
    25
open Metis_Clauses
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    26
open Sledgehammer_Util
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
    27
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    28
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    29
(** ATP problem **)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    30
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    31
datatype 'a atp_term = ATerm of 'a * 'a atp_term list
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    32
type 'a atp_literal = bool * 'a atp_term
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    33
datatype 'a problem_line = Cnf of string * kind * 'a atp_literal list
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    34
type 'a problem = (string * 'a problem_line list) list
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    35
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    36
fun string_for_atp_term (ATerm (s, [])) = s
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    37
  | string_for_atp_term (ATerm (s, ts)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    38
    s ^ "(" ^ commas (map string_for_atp_term ts) ^ ")"
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    39
fun string_for_atp_literal (pos, ATerm ("equal", [t1, t2])) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    40
    string_for_atp_term t1 ^ " " ^ (if pos then "=" else "!=") ^ " " ^
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    41
    string_for_atp_term t2
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    42
  | string_for_atp_literal (pos, t) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    43
    (if pos then "" else "~ ") ^ string_for_atp_term t
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    44
fun string_for_problem_line (Cnf (ident, kind, lits)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    45
  "cnf(" ^ ident ^ ", " ^
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    46
  (case kind of Axiom => "axiom" | Conjecture => "negated_conjecture") ^ ",\n" ^
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    47
  "    (" ^ space_implode " | " (map string_for_atp_literal lits) ^ ")).\n"
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    48
fun strings_for_problem problem =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    49
  "% This file was generated by Isabelle (most likely Sledgehammer)\n\
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    50
  \% " ^ timestamp () ^ "\n" ::
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    51
  maps (fn (_, []) => []
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    52
         | (heading, lines) =>
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    53
           "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    54
           map string_for_problem_line lines) problem
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    55
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    56
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    57
(** Nice names **)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    58
37624
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    59
type name_pool = string Symtab.table * string Symtab.table
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    60
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    61
fun empty_name_pool readable_names =
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    62
  if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
37624
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    63
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    64
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    65
fun pool_map f xs =
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    66
  pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    67
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    68
(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    69
   unreadable "op_1", "op_2", etc., in the problem files. *)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    70
val reserved_nice_names = ["equal", "op"]
37624
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    71
fun readable_name full_name s =
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    72
  if s = full_name then
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    73
    s
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    74
  else
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    75
    let
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    76
      val s = s |> Long_Name.base_name
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    77
                |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
    78
    in if member (op =) reserved_nice_names s then full_name else s end
37624
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    79
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    80
fun nice_name (full_name, _) NONE = (full_name, NONE)
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    81
  | nice_name (full_name, desired_name) (SOME the_pool) =
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    82
    case Symtab.lookup (fst the_pool) full_name of
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    83
      SOME nice_name => (nice_name, SOME the_pool)
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    84
    | NONE =>
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    85
      let
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    86
        val nice_prefix = readable_name full_name desired_name
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    87
        fun add j =
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    88
          let
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    89
            val nice_name = nice_prefix ^
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    90
                            (if j = 0 then "" else "_" ^ Int.toString j)
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    91
          in
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    92
            case Symtab.lookup (snd the_pool) nice_name of
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    93
              SOME full_name' =>
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    94
              if full_name = full_name' then (nice_name, the_pool)
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    95
              else add (j + 1)
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    96
            | NONE =>
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    97
              (nice_name,
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    98
               (Symtab.update_new (full_name, nice_name) (fst the_pool),
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
    99
                Symtab.update_new (nice_name, full_name) (snd the_pool)))
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
   100
          end
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
   101
      in add 0 |> apsnd SOME end
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
   102
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   103
fun nice_atp_term (ATerm (name, ts)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   104
  nice_name name ##>> pool_map nice_atp_term ts #>> ATerm
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   105
fun nice_atp_literal (pos, t) = nice_atp_term t #>> pair pos
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   106
fun nice_problem_line (Cnf (ident, kind, lits)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   107
  pool_map nice_atp_literal lits #>> (fn lits => Cnf (ident, kind, lits))
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   108
val nice_problem =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   109
  pool_map (fn (heading, lines) =>
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   110
               pool_map nice_problem_line lines #>> pair heading)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   111
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   112
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   113
(** Sledgehammer stuff **)
37520
9fc2ae73c5ca fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem
blanchet
parents: 37519
diff changeset
   114
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   115
val clause_prefix = "cls_"
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   116
val arity_clause_prefix = "clsarity_"
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   117
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   118
fun hol_ident axiom_name clause_id =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   119
  clause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   120
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   121
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   122
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   123
fun atp_term_for_combtyp (TyVar name) = ATerm (name, [])
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   124
  | atp_term_for_combtyp (TyFree name) = ATerm (name, [])
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   125
  | atp_term_for_combtyp (TyConstr (name, tys)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   126
    ATerm (name, map atp_term_for_combtyp tys)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   127
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   128
fun atp_term_for_combterm full_types top_level u =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   129
  let
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   130
    val (head, args) = strip_combterm_comb u
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   131
    val (x, ty_args) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   132
      case head of
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   133
        CombConst (name, _, ty_args) =>
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   134
        if fst name = "equal" then
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   135
          (if top_level andalso length args = 2 then name
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   136
           else ("c_fequal", @{const_name fequal}), [])
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   137
        else
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   138
          (name, if full_types then [] else ty_args)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   139
      | CombVar (name, _) => (name, [])
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   140
      | CombApp _ => raise Fail "impossible \"CombApp\""
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   141
    val t = ATerm (x, map atp_term_for_combtyp ty_args @
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   142
                      map (atp_term_for_combterm full_types false) args)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   143
  in
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   144
    if full_types then wrap_type (atp_term_for_combtyp (type_of_combterm u)) t
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   145
    else t
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   146
  end
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   147
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   148
fun atp_literal_for_literal full_types (Literal (pos, t)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   149
  (pos, atp_term_for_combterm full_types true t)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   150
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   151
fun atp_literal_for_type_literal pos (TyLitVar (class, name)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   152
    (pos, ATerm (class, [ATerm (name, [])]))
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   153
  | atp_literal_for_type_literal pos (TyLitFree (class, name)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   154
    (pos, ATerm (class, [ATerm (name, [])]))
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   155
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   156
fun atp_literals_for_axiom full_types
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   157
        (HOLClause {literals, ctypes_sorts, ...}) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   158
  map (atp_literal_for_literal full_types) literals @
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   159
  map (atp_literal_for_type_literal false)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   160
      (type_literals_for_types ctypes_sorts)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   161
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   162
fun problem_line_for_axiom full_types
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   163
        (clause as HOLClause {axiom_name, clause_id, kind, ...}) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   164
  Cnf (hol_ident axiom_name clause_id, kind,
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   165
       atp_literals_for_axiom full_types clause)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   166
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   167
fun problem_line_for_classrel
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   168
        (ClassrelClause {axiom_name, subclass, superclass, ...}) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   169
  let val ty_arg = ATerm (("T", "T"), []) in
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   170
    Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])),
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   171
                                      (true, ATerm (superclass, [ty_arg]))])
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   172
  end
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   173
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   174
fun atp_literal_for_arity_literal (TConsLit (c, t, args)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   175
    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   176
  | atp_literal_for_arity_literal (TVarLit (c, sort)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   177
    (false, ATerm (c, [ATerm (sort, [])]))
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   178
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   179
fun problem_line_for_arity (ArityClause {axiom_name, conclLit, premLits, ...}) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   180
  Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   181
       map atp_literal_for_arity_literal (conclLit :: premLits))
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   182
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   183
fun problem_line_for_conjecture full_types
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   184
        (clause as HOLClause {axiom_name, clause_id, kind, literals, ...}) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   185
  Cnf (hol_ident axiom_name clause_id, kind,
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   186
       map (atp_literal_for_literal full_types) literals)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   187
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   188
fun atp_free_type_literals_for_conjecture (HOLClause {ctypes_sorts, ...}) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   189
  map (atp_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   190
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   191
fun problem_line_for_free_type lit = Cnf ("tfree_tcs", Conjecture, [lit])
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   192
fun problem_lines_for_free_types conjectures =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   193
  let
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   194
    val litss = map atp_free_type_literals_for_conjecture conjectures
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   195
    val lits = fold (union (op =)) litss []
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   196
  in map problem_line_for_free_type lits end
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   197
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   198
(** "hBOOL" and "hAPP" **)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   199
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   200
type const_info = {min_arity: int, max_arity: int, sub_level: bool}
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   201
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   202
fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   203
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   204
fun consider_term top_level (ATerm ((s, _), ts)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   205
  (if is_atp_variable s then
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   206
     I
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   207
   else
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   208
     let val n = length ts in
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   209
       Symtab.map_default
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   210
           (s, {min_arity = n, max_arity = 0, sub_level = false})
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   211
           (fn {min_arity, max_arity, sub_level} =>
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   212
               {min_arity = Int.min (n, min_arity),
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   213
                max_arity = Int.max (n, max_arity),
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   214
                sub_level = sub_level orelse not top_level})
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   215
     end)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   216
  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   217
fun consider_literal (_, t) = consider_term true t
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   218
fun consider_problem_line (Cnf (_, _, lits)) = fold consider_literal lits
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   219
val consider_problem = fold (fold consider_problem_line o snd)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   220
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   221
fun const_table_for_problem explicit_apply problem =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   222
  if explicit_apply then NONE
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   223
  else SOME (Symtab.empty |> consider_problem problem)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   224
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   225
val tc_fun = make_fixed_type_const @{type_name fun}
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   226
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   227
fun min_arity_of thy full_types NONE s =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   228
    (if s = "equal" orelse s = type_wrapper_name orelse
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   229
        String.isPrefix type_const_prefix s orelse
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   230
        String.isPrefix class_prefix s then
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   231
       16383 (* large number *)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   232
     else if full_types then
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   233
       0
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   234
     else case strip_prefix const_prefix s of
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   235
       SOME s' => num_type_args thy (invert_const s')
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   236
     | NONE => 0)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   237
  | min_arity_of _ _ (SOME the_const_tab) s =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   238
    case Symtab.lookup the_const_tab s of
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   239
      SOME ({min_arity, ...} : const_info) => min_arity
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   240
    | NONE => 0
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   241
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   242
fun full_type_of (ATerm ((s, _), [ty, _])) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   243
    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   244
  | full_type_of _ = raise Fail "expected type wrapper"
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   245
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   246
fun list_hAPP_rev _ t1 [] = t1
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   247
  | list_hAPP_rev NONE t1 (t2 :: ts2) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   248
    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   249
  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   250
    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   251
                         [full_type_of t2, ty]) in
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   252
      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   253
    end
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   254
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   255
fun repair_applications_in_term thy full_types const_tab =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   256
  let
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   257
    fun aux opt_ty (ATerm (name as (s, _), ts)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   258
      if s = type_wrapper_name then
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   259
        case ts of
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   260
          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   261
        | _ => raise Fail "malformed type wrapper"
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   262
      else
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   263
        let
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   264
          val ts = map (aux NONE) ts
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   265
          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   266
        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   267
  in aux NONE end
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   268
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   269
fun boolify t = ATerm (`I "hBOOL", [t])
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   270
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   271
(* True if the constant ever appears outside of the top-level position in
37520
9fc2ae73c5ca fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem
blanchet
parents: 37519
diff changeset
   272
   literals, or if it appears with different arities (e.g., because of different
9fc2ae73c5ca fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem
blanchet
parents: 37519
diff changeset
   273
   type instantiations). If false, the constant always receives all of its
9fc2ae73c5ca fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem
blanchet
parents: 37519
diff changeset
   274
   arguments and is used as a predicate. *)
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   275
fun is_predicate NONE s =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   276
    s = "equal" orelse String.isPrefix type_const_prefix s orelse
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   277
    String.isPrefix class_prefix s
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   278
  | is_predicate (SOME the_const_tab) s =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   279
    case Symtab.lookup the_const_tab s of
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   280
      SOME {min_arity, max_arity, sub_level} =>
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   281
      not sub_level andalso min_arity = max_arity
37520
9fc2ae73c5ca fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem
blanchet
parents: 37519
diff changeset
   282
    | NONE => false
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   283
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   284
fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   285
  if s = type_wrapper_name then
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   286
    case ts of
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   287
      [_, t' as ATerm ((s', _), _)] =>
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   288
      if is_predicate const_tab s' then t' else boolify t
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   289
    | _ => raise Fail "malformed type wrapper"
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   290
  else
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   291
    t |> not (is_predicate const_tab s) ? boolify
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   292
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   293
fun repair_literal thy full_types const_tab (pos, t) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   294
  (pos, t |> repair_applications_in_term thy full_types const_tab
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   295
          |> repair_predicates_in_term const_tab)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   296
fun repair_problem_line thy full_types const_tab (Cnf (ident, kind, lits)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   297
  Cnf (ident, kind, map (repair_literal thy full_types const_tab) lits)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   298
val repair_problem_with_const_table = map o apsnd o map ooo repair_problem_line
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   299
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   300
fun repair_problem thy full_types explicit_apply problem =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   301
  repair_problem_with_const_table thy full_types
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   302
      (const_table_for_problem explicit_apply problem) problem
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   303
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   304
fun write_tptp_file thy readable_names full_types explicit_apply file
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   305
                    (conjectures, axiom_clauses, extra_clauses, helper_clauses,
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   306
                     classrel_clauses, arity_clauses) =
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   307
  let
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   308
    val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   309
    val classrel_lines = map problem_line_for_classrel classrel_clauses
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   310
    val arity_lines = map problem_line_for_arity arity_clauses
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   311
    val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   312
    val conjecture_lines =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   313
      map (problem_line_for_conjecture full_types) conjectures
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   314
    val tfree_lines = problem_lines_for_free_types conjectures
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   315
    val problem = [("Relevant facts", axiom_lines),
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   316
                   ("Class relationships", classrel_lines),
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   317
                   ("Arity declarations", arity_lines),
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   318
                   ("Helper facts", helper_lines),
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   319
                   ("Conjectures", conjecture_lines),
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   320
                   ("Type variables", tfree_lines)]
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   321
                  |> repair_problem thy full_types explicit_apply
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   322
    val (problem, pool) = nice_problem problem (empty_name_pool readable_names)
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   323
    val conjecture_offset =
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   324
      length axiom_lines + length classrel_lines + length arity_lines
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   325
      + length helper_lines
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   326
    val _ = File.write_list file (strings_for_problem problem)
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   327
  in (pool, conjecture_offset) end
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   328
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   329
end;