author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 37703  b4c799bab553 
child 37922  ff56c361d75b 
permissions  rwrr 
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  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  59 
type name_pool = string Symtab.table * string Symtab.table 
60 

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  63 

64 
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs 

65 
fun pool_map f xs = 

66 
pool_fold (fn x => fn ys => fn pool => f x pool >> (fn y => y :: ys)) xs [] 

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  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  79 

80 
fun nice_name (full_name, _) NONE = (full_name, NONE) 

81 
 nice_name (full_name, desired_name) (SOME the_pool) = 

82 
case Symtab.lookup (fst the_pool) full_name of 

83 
SOME nice_name => (nice_name, SOME the_pool) 

84 
 NONE => 

85 
let 

86 
val nice_prefix = readable_name full_name desired_name 

87 
fun add j = 

88 
let 

89 
val nice_name = nice_prefix ^ 

90 
(if j = 0 then "" else "_" ^ Int.toString j) 

91 
in 

92 
case Symtab.lookup (snd the_pool) nice_name of 

93 
SOME full_name' => 

94 
if full_name = full_name' then (nice_name, the_pool) 

95 
else add (j + 1) 

96 
 NONE => 

97 
(nice_name, 

98 
(Symtab.update_new (full_name, nice_name) (fst the_pool), 

99 
Symtab.update_new (nice_name, full_name) (snd the_pool))) 

100 
end 

101 
in add 0 > apsnd SOME end 

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 nary 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 toplevel position in 
37520
9fc2ae73c5ca
fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for nary 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 nary 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 nary 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 nary 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; 