author | blanchet |
Mon, 26 Jul 2010 11:26:47 +0200 | |
changeset 37993 | bb39190370fe |
parent 37992 | 7911e78a7122 |
child 37994 | b04307085a09 |
permissions | -rw-r--r-- |
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 |
37925 | 10 |
type class_rel_clause = Metis_Clauses.class_rel_clause |
37578
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 |
37922
ff56c361d75b
renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators
blanchet
parents:
37703
diff
changeset
|
12 |
type fol_clause = Metis_Clauses.fol_clause |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
13 |
|
37992 | 14 |
datatype 'a fo_term = ATerm of 'a * 'a fo_term list |
15 |
datatype quantifier = AForall | AExists |
|
16 |
datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff |
|
17 |
datatype 'a formula = |
|
18 |
AQuant of quantifier * 'a list * 'a formula | |
|
19 |
AConn of connective * 'a formula list | |
|
20 |
APred of 'a fo_term |
|
21 |
||
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37961
diff
changeset
|
22 |
val axiom_prefix : string |
37992 | 23 |
val conjecture_prefix : string |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
24 |
val write_tptp_file : |
37993
bb39190370fe
generate close formulas for SPASS, but not for the others (to avoid clutter)
blanchet
parents:
37992
diff
changeset
|
25 |
theory -> bool -> bool -> bool -> bool -> Path.T |
37922
ff56c361d75b
renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators
blanchet
parents:
37703
diff
changeset
|
26 |
-> fol_clause list * fol_clause list * fol_clause list * fol_clause list |
37925 | 27 |
* class_rel_clause list * arity_clause list |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
28 |
-> string Symtab.table * int |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
29 |
end; |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
30 |
|
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
31 |
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
|
32 |
struct |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
33 |
|
37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset
|
34 |
open Metis_Clauses |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
35 |
open Sledgehammer_Util |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
36 |
|
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
37 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
38 |
(** ATP problem **) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
39 |
|
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
40 |
datatype 'a fo_term = ATerm of 'a * 'a fo_term list |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
41 |
datatype quantifier = AForall | AExists |
37992 | 42 |
datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
43 |
datatype 'a formula = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
44 |
AQuant of quantifier * 'a list * 'a formula | |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
45 |
AConn of connective * 'a formula list | |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
46 |
APred of 'a fo_term |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
47 |
|
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
48 |
fun mk_anot phi = AConn (ANot, [phi]) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
49 |
|
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
50 |
datatype 'a problem_line = Fof of string * kind * 'a formula |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
51 |
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
|
52 |
|
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
53 |
fun string_for_term (ATerm (s, [])) = s |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
54 |
| string_for_term (ATerm (s, ts)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
55 |
if s = "equal" then space_implode " = " (map string_for_term ts) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
56 |
else s ^ "(" ^ commas (map string_for_term ts) ^ ")" |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
57 |
fun string_for_quantifier AForall = "!" |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
58 |
| string_for_quantifier AExists = "?" |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
59 |
fun string_for_connective ANot = "~" |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
60 |
| string_for_connective AAnd = "&" |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
61 |
| string_for_connective AOr = "|" |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
62 |
| string_for_connective AImplies = "=>" |
37992 | 63 |
| string_for_connective AIf = "<=" |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
64 |
| string_for_connective AIff = "<=>" |
37992 | 65 |
| string_for_connective ANotIff = "<~>" |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
66 |
fun string_for_formula (AQuant (q, xs, phi)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
67 |
string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^ |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
68 |
string_for_formula phi |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
69 |
| string_for_formula (AConn (c, [phi])) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
70 |
string_for_connective c ^ " " ^ string_for_formula phi |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
71 |
| string_for_formula (AConn (c, phis)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
72 |
"(" ^ space_implode (" " ^ string_for_connective c ^ " ") |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
73 |
(map string_for_formula phis) ^ ")" |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
74 |
| string_for_formula (APred tm) = string_for_term tm |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
75 |
|
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
76 |
fun string_for_problem_line (Fof (ident, kind, phi)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
77 |
"fof(" ^ ident ^ ", " ^ |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
78 |
(case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^ |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
79 |
" (" ^ string_for_formula phi ^ ")).\n" |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
80 |
fun strings_for_problem problem = |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
81 |
"% 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
|
82 |
\% " ^ timestamp () ^ "\n" :: |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
83 |
maps (fn (_, []) => [] |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
84 |
| (heading, lines) => |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
85 |
"\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" :: |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
86 |
map string_for_problem_line lines) problem |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
87 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
88 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
89 |
(** Nice names **) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
90 |
|
37624 | 91 |
fun empty_name_pool readable_names = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
92 |
if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE |
37624 | 93 |
|
94 |
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs |
|
95 |
fun pool_map f xs = |
|
96 |
pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs [] |
|
97 |
||
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
98 |
(* "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
|
99 |
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
|
100 |
val reserved_nice_names = ["equal", "op"] |
37624 | 101 |
fun readable_name full_name s = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
102 |
if s = full_name then |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
103 |
s |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
104 |
else |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
105 |
let |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
106 |
val s = s |> Long_Name.base_name |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
107 |
|> 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
|
108 |
in if member (op =) reserved_nice_names s then full_name else s end |
37624 | 109 |
|
110 |
fun nice_name (full_name, _) NONE = (full_name, NONE) |
|
111 |
| nice_name (full_name, desired_name) (SOME the_pool) = |
|
112 |
case Symtab.lookup (fst the_pool) full_name of |
|
113 |
SOME nice_name => (nice_name, SOME the_pool) |
|
114 |
| NONE => |
|
115 |
let |
|
116 |
val nice_prefix = readable_name full_name desired_name |
|
117 |
fun add j = |
|
118 |
let |
|
119 |
val nice_name = nice_prefix ^ |
|
120 |
(if j = 0 then "" else "_" ^ Int.toString j) |
|
121 |
in |
|
122 |
case Symtab.lookup (snd the_pool) nice_name of |
|
123 |
SOME full_name' => |
|
124 |
if full_name = full_name' then (nice_name, the_pool) |
|
125 |
else add (j + 1) |
|
126 |
| NONE => |
|
127 |
(nice_name, |
|
128 |
(Symtab.update_new (full_name, nice_name) (fst the_pool), |
|
129 |
Symtab.update_new (nice_name, full_name) (snd the_pool))) |
|
130 |
end |
|
131 |
in add 0 |> apsnd SOME end |
|
132 |
||
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
133 |
|
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
134 |
fun nice_term (ATerm (name, ts)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
135 |
nice_name name ##>> pool_map nice_term ts #>> ATerm |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
136 |
fun nice_formula (AQuant (q, xs, phi)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
137 |
pool_map nice_name xs ##>> nice_formula phi |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
138 |
#>> (fn (xs, phi) => AQuant (q, xs, phi)) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
139 |
| nice_formula (AConn (c, phis)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
140 |
pool_map nice_formula phis #>> curry AConn c |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
141 |
| nice_formula (APred tm) = nice_term tm #>> APred |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
142 |
fun nice_problem_line (Fof (ident, kind, phi)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
143 |
nice_formula phi #>> (fn phi => Fof (ident, kind, phi)) |
37931 | 144 |
fun nice_problem problem = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
145 |
pool_map (fn (heading, lines) => |
37931 | 146 |
pool_map nice_problem_line lines #>> pair heading) problem |
37643
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 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
149 |
(** 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
|
150 |
|
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37961
diff
changeset
|
151 |
val axiom_prefix = "ax_" |
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37961
diff
changeset
|
152 |
val conjecture_prefix = "conj_" |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
153 |
val arity_clause_prefix = "clsarity_" |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
154 |
|
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
155 |
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
|
156 |
|
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
157 |
fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
158 |
| fo_term_for_combtyp (CombTFree name) = ATerm (name, []) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
159 |
| fo_term_for_combtyp (CombType (name, tys)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
160 |
ATerm (name, map fo_term_for_combtyp tys) |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
161 |
|
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
162 |
fun fo_term_for_combterm full_types top_level u = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
163 |
let |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
164 |
val (head, args) = strip_combterm_comb u |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
165 |
val (x, ty_args) = |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
166 |
case head of |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
167 |
CombConst (name, _, ty_args) => |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
168 |
if fst name = "equal" then |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
169 |
(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
|
170 |
else ("c_fequal", @{const_name fequal}), []) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
171 |
else |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
172 |
(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
|
173 |
| CombVar (name, _) => (name, []) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
174 |
| CombApp _ => raise Fail "impossible \"CombApp\"" |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
175 |
val t = ATerm (x, map fo_term_for_combtyp ty_args @ |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
176 |
map (fo_term_for_combterm full_types false) args) |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
177 |
in |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
178 |
if full_types then wrap_type (fo_term_for_combtyp (type_of_combterm u)) t |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
179 |
else t |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
180 |
end |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
181 |
|
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
182 |
fun fo_literal_for_literal full_types (FOLLiteral (pos, t)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
183 |
(pos, fo_term_for_combterm full_types true t) |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
184 |
|
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
185 |
fun fo_literal_for_type_literal pos (TyLitVar (class, name)) = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
186 |
(pos, ATerm (class, [ATerm (name, [])])) |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
187 |
| fo_literal_for_type_literal pos (TyLitFree (class, name)) = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
188 |
(pos, ATerm (class, [ATerm (name, [])])) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
189 |
|
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
190 |
fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
191 |
fun formula_for_fo_literals [] = APred (ATerm (("$false", "$false"), [])) |
37992 | 192 |
| formula_for_fo_literals [lit] = formula_for_fo_literal lit |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
193 |
| formula_for_fo_literals (lit :: lits) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
194 |
AConn (AOr, [formula_for_fo_literal lit, formula_for_fo_literals lits]) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
195 |
|
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
196 |
fun formula_for_axiom full_types (FOLClause {literals, ctypes_sorts, ...}) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
197 |
map (fo_literal_for_literal full_types) literals @ |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
198 |
map (fo_literal_for_type_literal false) |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
199 |
(type_literals_for_types ctypes_sorts) |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
200 |
|> formula_for_fo_literals |
37643
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 problem_line_for_axiom full_types |
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37961
diff
changeset
|
203 |
(clause as FOLClause {axiom_name, kind, ...}) = |
37992 | 204 |
Fof (axiom_prefix ^ ascii_of axiom_name, kind, |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
205 |
formula_for_axiom full_types clause) |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
206 |
|
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
207 |
fun problem_line_for_class_rel_clause |
37925 | 208 |
(ClassRelClause {axiom_name, subclass, superclass, ...}) = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
209 |
let val ty_arg = ATerm (("T", "T"), []) in |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
210 |
Fof (ascii_of axiom_name, Axiom, |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
211 |
AConn (AImplies, [APred (ATerm (subclass, [ty_arg])), |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
212 |
APred (ATerm (superclass, [ty_arg]))])) |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
213 |
end |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
214 |
|
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
215 |
fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
216 |
(true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
217 |
| fo_literal_for_arity_literal (TVarLit (c, sort)) = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
218 |
(false, ATerm (c, [ATerm (sort, [])])) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
219 |
|
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
220 |
fun problem_line_for_arity_clause |
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
221 |
(ArityClause {axiom_name, conclLit, premLits, ...}) = |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
222 |
Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
223 |
map fo_literal_for_arity_literal (conclLit :: premLits) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
224 |
|> formula_for_fo_literals) |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
225 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
226 |
fun problem_line_for_conjecture full_types |
37992 | 227 |
(clause as FOLClause {clause_id, kind, literals, ...}) = |
228 |
Fof (conjecture_prefix ^ Int.toString clause_id, |
|
229 |
kind, map (fo_literal_for_literal full_types) literals |
|
230 |
|> formula_for_fo_literals |> mk_anot) |
|
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
231 |
|
37922
ff56c361d75b
renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators
blanchet
parents:
37703
diff
changeset
|
232 |
fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) = |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
233 |
map (fo_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
|
234 |
|
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
235 |
fun problem_line_for_free_type lit = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
236 |
Fof ("tfree_tcs", Conjecture, formula_for_fo_literal lit) |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
237 |
fun problem_lines_for_free_types conjectures = |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
238 |
let |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
239 |
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
|
240 |
val lits = fold (union (op =)) litss [] |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
241 |
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
|
242 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
243 |
(** "hBOOL" and "hAPP" **) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
244 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
245 |
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
|
246 |
|
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
247 |
fun is_variable s = Char.isUpper (String.sub (s, 0)) |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
248 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
249 |
fun consider_term top_level (ATerm ((s, _), ts)) = |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
250 |
(if is_variable s then |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
251 |
I |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
252 |
else |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
253 |
let val n = length ts in |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
254 |
Symtab.map_default |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
255 |
(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
|
256 |
(fn {min_arity, max_arity, sub_level} => |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
257 |
{min_arity = Int.min (n, min_arity), |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
258 |
max_arity = Int.max (n, max_arity), |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
259 |
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
|
260 |
end) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
261 |
#> fold (consider_term (top_level andalso s = type_wrapper_name)) ts |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
262 |
fun consider_formula (AQuant (_, _, phi)) = consider_formula phi |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
263 |
| consider_formula (AConn (_, phis)) = fold consider_formula phis |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
264 |
| consider_formula (APred tm) = consider_term true tm |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
265 |
|
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
266 |
fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi |
37931 | 267 |
fun consider_problem problem = fold (fold consider_problem_line o snd) problem |
37643
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 const_table_for_problem explicit_apply problem = |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
270 |
if explicit_apply then NONE |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
271 |
else SOME (Symtab.empty |> consider_problem problem) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
272 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
273 |
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
|
274 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
275 |
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
|
276 |
(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
|
277 |
String.isPrefix type_const_prefix s orelse |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
278 |
String.isPrefix class_prefix s then |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
279 |
16383 (* large number *) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
280 |
else if full_types then |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
281 |
0 |
37992 | 282 |
else case strip_prefix_and_undo_ascii const_prefix s of |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
283 |
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
|
284 |
| NONE => 0) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
285 |
| 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
|
286 |
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
|
287 |
SOME ({min_arity, ...} : const_info) => min_arity |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
288 |
| NONE => 0 |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
289 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
290 |
fun full_type_of (ATerm ((s, _), [ty, _])) = |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
291 |
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
|
292 |
| 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
|
293 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
294 |
fun list_hAPP_rev _ t1 [] = t1 |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
295 |
| list_hAPP_rev NONE t1 (t2 :: ts2) = |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
296 |
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
|
297 |
| 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
|
298 |
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
|
299 |
[full_type_of t2, ty]) in |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
300 |
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
|
301 |
end |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
302 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
303 |
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
|
304 |
let |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
305 |
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
|
306 |
if s = type_wrapper_name then |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
307 |
case ts of |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
308 |
[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
|
309 |
| _ => raise Fail "malformed type wrapper" |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
310 |
else |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
311 |
let |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
312 |
val ts = map (aux NONE) ts |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
313 |
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
|
314 |
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
|
315 |
in aux NONE end |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
316 |
|
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
317 |
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
|
318 |
|
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
319 |
(* 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
|
320 |
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
|
321 |
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
|
322 |
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
|
323 |
fun is_predicate NONE s = |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
324 |
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
|
325 |
String.isPrefix class_prefix s |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
326 |
| is_predicate (SOME the_const_tab) s = |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
327 |
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
|
328 |
SOME {min_arity, max_arity, sub_level} => |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
329 |
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
|
330 |
| NONE => false |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
331 |
|
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
332 |
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
|
333 |
if s = type_wrapper_name then |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
334 |
case ts of |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
335 |
[_, t' as ATerm ((s', _), _)] => |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
336 |
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
|
337 |
| _ => 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
|
338 |
else |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
339 |
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
|
340 |
|
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
341 |
fun close_universally phi = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
342 |
let |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
343 |
fun term_vars bounds (ATerm (name as (s, _), tms)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
344 |
(is_variable s andalso not (member (op =) bounds name)) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
345 |
? insert (op =) name |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
346 |
#> fold (term_vars bounds) tms |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
347 |
fun formula_vars bounds (AQuant (q, xs, phi)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
348 |
formula_vars (xs @ bounds) phi |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
349 |
| formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
350 |
| formula_vars bounds (APred tm) = term_vars bounds tm |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
351 |
in |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
352 |
case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
353 |
end |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
354 |
|
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
355 |
fun repair_formula thy explicit_forall full_types const_tab = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
356 |
let |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
357 |
fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
358 |
| aux (AConn (c, phis)) = AConn (c, map aux phis) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
359 |
| aux (APred tm) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
360 |
APred (tm |> repair_applications_in_term thy full_types const_tab |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
361 |
|> repair_predicates_in_term const_tab) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
362 |
in aux #> explicit_forall ? close_universally end |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
363 |
|
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
364 |
fun repair_problem_line thy explicit_forall full_types const_tab |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
365 |
(Fof (ident, kind, phi)) = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
366 |
Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
367 |
val repair_problem_with_const_table = map o apsnd o map oooo repair_problem_line |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
368 |
|
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
369 |
fun repair_problem thy explicit_forall full_types explicit_apply problem = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
370 |
repair_problem_with_const_table thy explicit_forall full_types |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
371 |
(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
|
372 |
|
37993
bb39190370fe
generate close formulas for SPASS, but not for the others (to avoid clutter)
blanchet
parents:
37992
diff
changeset
|
373 |
fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply |
bb39190370fe
generate close formulas for SPASS, but not for the others (to avoid clutter)
blanchet
parents:
37992
diff
changeset
|
374 |
file (conjectures, axiom_clauses, extra_clauses, |
bb39190370fe
generate close formulas for SPASS, but not for the others (to avoid clutter)
blanchet
parents:
37992
diff
changeset
|
375 |
helper_clauses, class_rel_clauses, arity_clauses) = |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
376 |
let |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
377 |
val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
378 |
val class_rel_lines = |
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
379 |
map problem_line_for_class_rel_clause class_rel_clauses |
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
380 |
val arity_lines = map problem_line_for_arity_clause arity_clauses |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
381 |
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
|
382 |
val conjecture_lines = |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
383 |
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
|
384 |
val tfree_lines = problem_lines_for_free_types conjectures |
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
385 |
val problem = |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
386 |
[("Relevant facts", axiom_lines), |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
387 |
("Class relationships", class_rel_lines), |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
388 |
("Arity declarations", arity_lines), |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
389 |
("Helper facts", helper_lines), |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
390 |
("Conjectures", conjecture_lines), |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
391 |
("Type variables", tfree_lines)] |
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset
|
392 |
|> repair_problem thy explicit_forall full_types explicit_apply |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
393 |
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
|
394 |
val conjecture_offset = |
37925 | 395 |
length axiom_lines + length class_rel_lines + length arity_lines |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
396 |
+ length helper_lines |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset
|
397 |
val _ = File.write_list file (strings_for_problem problem) |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
398 |
in |
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
399 |
(case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, |
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
400 |
conjecture_offset) |
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
401 |
end |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
402 |
|
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset
|
403 |
end; |