author  blanchet 
Thu, 29 Apr 2010 10:25:26 +0200  
changeset 36556  81dc2c20f052 
parent 36493  a3357a631b96 
child 36692  54b64d4ad524 
permissions  rwrr 
35826  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML 
33311  2 
Author: Jia Meng, Cambridge University Computer Laboratory 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36378
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
15347  4 

33311  5 
Storing/printing FOL clauses and arity clauses. Typed equality is 
6 
treated differently. 

7 

36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

8 
FIXME: combine with sledgehammer_hol_clause! 
15347  9 
*) 
10 

35826  11 
signature SLEDGEHAMMER_FOL_CLAUSE = 
24310  12 
sig 
13 
val schematic_var_prefix: string 

14 
val fixed_var_prefix: string 

15 
val tvar_prefix: string 

16 
val tfree_prefix: string 

17 
val clause_prefix: string 

18 
val const_prefix: string 

19 
val tconst_prefix: string 

20 
val class_prefix: string 

21 
val union_all: ''a list list > ''a list 

22 
val const_trans_table: string Symtab.table 

23 
val type_const_trans_table: string Symtab.table 

24 
val ascii_of: string > string 

25 
val undo_ascii_of: string > string 

26 
val paren_pack : string list > string 

27 
val make_schematic_var : string * int > string 

18868  28 
val make_fixed_var : string > string 
29 
val make_schematic_type_var : string * int > string 

24310  30 
val make_fixed_type_var : string > string 
30151  31 
val make_fixed_const : bool > string > string 
32 
val make_fixed_type_const : bool > string > string 

18868  33 
val make_type_class : string > string 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

34 
type name = string * string 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

35 
type name_pool = string Symtab.table * string Symtab.table 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

36 
val empty_name_pool : bool > name_pool option 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

37 
val pool_map : ('a > 'b > 'c * 'b) > 'a list > 'b > 'c list * 'b 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

38 
val nice_name : name > name_pool option > string * name_pool option 
24310  39 
datatype kind = Axiom  Conjecture 
40 
type axiom_name = string 

41 
datatype fol_type = 

36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

42 
TyVar of name  
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

43 
TyFree of name  
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

44 
TyConstr of name * fol_type list 
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

45 
val string_of_fol_type : 
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

46 
fol_type > name_pool option > string * name_pool option 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

47 
datatype type_literal = 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

48 
TyLitVar of string * name  
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

49 
TyLitFree of string * name 
24310  50 
exception CLAUSE of string * term 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

51 
val add_type_literals : typ list > type_literal list 
24940  52 
val get_tvar_strs: typ list > string list 
24310  53 
datatype arLit = 
54 
TConsLit of class * string * string list 

55 
 TVarLit of class * string 

35865  56 
datatype arity_clause = ArityClause of 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

57 
{axiom_name: axiom_name, conclLit: arLit, premLits: arLit list} 
35865  58 
datatype classrel_clause = ClassrelClause of 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

59 
{axiom_name: axiom_name, subclass: class, superclass: class} 
35865  60 
val make_classrel_clauses: theory > class list > class list > classrel_clause list 
61 
val make_arity_clauses_dfg: bool > theory > string list > class list > class list * arity_clause list 

62 
val make_arity_clauses: theory > string list > class list > class list * arity_clause list 

36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

63 
val add_type_sort_preds: typ > int Symtab.table > int Symtab.table 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

64 
val add_classrel_clause_preds : 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

65 
classrel_clause > int Symtab.table > int Symtab.table 
24310  66 
val class_of_arityLit: arLit > class 
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

67 
val add_arity_clause_preds: arity_clause > int Symtab.table > int Symtab.table 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

68 
val add_fol_type_funcs: fol_type > int Symtab.table > int Symtab.table 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

69 
val add_arity_clause_funcs: 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

70 
arity_clause > int Symtab.table > int Symtab.table 
24310  71 
val init_functab: int Symtab.table 
19719  72 
val dfg_sign: bool > string > string 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

73 
val dfg_of_type_literal: bool > type_literal > string 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

74 
val gen_dfg_cls: int * string * kind * string list * string list * string list > string 
24310  75 
val string_of_preds: (string * Int.int) list > string 
76 
val string_of_funcs: (string * int) list > string 

77 
val string_of_symbols: string > string > string 

19719  78 
val string_of_start: string > string 
79 
val string_of_descrip : string > string 

24310  80 
val dfg_tfree_clause : string > string 
35865  81 
val dfg_classrel_clause: classrel_clause > string 
82 
val dfg_arity_clause: arity_clause > string 

24310  83 
val tptp_sign: bool > string > string 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

84 
val tptp_of_type_literal : 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

85 
bool > type_literal > name_pool option > string * name_pool option 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

86 
val gen_tptp_cls : int * string * kind * string list * string list > string 
24310  87 
val tptp_tfree_clause : string > string 
35865  88 
val tptp_arity_clause : arity_clause > string 
89 
val tptp_classrel_clause : classrel_clause > string 

24310  90 
end 
15347  91 

35826  92 
structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE = 
15347  93 
struct 
94 

36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36062
diff
changeset

95 
open Sledgehammer_Util 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36062
diff
changeset

96 

15347  97 
val schematic_var_prefix = "V_"; 
98 
val fixed_var_prefix = "v_"; 

99 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

100 
val tvar_prefix = "T_"; 
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

101 
val tfree_prefix = "t_"; 
15347  102 

24310  103 
val clause_prefix = "cls_"; 
104 
val arclause_prefix = "clsarity_" 

17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

105 
val clrelclause_prefix = "clsrel_"; 
15347  106 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

107 
val const_prefix = "c_"; 
24310  108 
val tconst_prefix = "tc_"; 
109 
val class_prefix = "class_"; 

15347  110 

36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

111 
fun union_all xss = fold (union (op =)) xss [] 
17775  112 

36493
a3357a631b96
reintroduced short names for HOL>FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset

113 
(* Readable names for the more common symbolic functions. Do not mess with the 
a3357a631b96
reintroduced short names for HOL>FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset

114 
last six entries of the table unless you know what you are doing. *) 
15347  115 
val const_trans_table = 
35865  116 
Symtab.make [(@{const_name "op ="}, "equal"), 
117 
(@{const_name "op &"}, "and"), 

118 
(@{const_name "op "}, "or"), 

119 
(@{const_name "op >"}, "implies"), 

36493
a3357a631b96
reintroduced short names for HOL>FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset

120 
(@{const_name "op :"}, "in"), 
a3357a631b96
reintroduced short names for HOL>FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset

121 
(@{const_name fequal}, "fequal"), 
a3357a631b96
reintroduced short names for HOL>FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset

122 
(@{const_name COMBI}, "COMBI"), 
a3357a631b96
reintroduced short names for HOL>FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset

123 
(@{const_name COMBK}, "COMBK"), 
a3357a631b96
reintroduced short names for HOL>FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset

124 
(@{const_name COMBB}, "COMBB"), 
a3357a631b96
reintroduced short names for HOL>FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset

125 
(@{const_name COMBC}, "COMBC"), 
a3357a631b96
reintroduced short names for HOL>FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset

126 
(@{const_name COMBS}, "COMBS")] 
15347  127 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

128 
val type_const_trans_table = 
36476
a04cf4704668
in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
blanchet
parents:
36393
diff
changeset

129 
Symtab.make [(@{type_name "*"}, "prod"), 
a04cf4704668
in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
blanchet
parents:
36393
diff
changeset

130 
(@{type_name "+"}, "sum")] 
15347  131 

15610  132 
(*Escaping of special characters. 
133 
Alphanumeric characters are left unchanged. 

134 
The character _ goes to __ 

135 
Characters in the range ASCII space to / go to _A to _P, respectively. 

24183  136 
Other printing characters go to _nnn where nnn is the decimal ASCII code.*) 
137 
val A_minus_space = Char.ord #"A"  Char.ord #" "; 

15610  138 

24183  139 
fun stringN_of_int 0 _ = "" 
140 
 stringN_of_int k n = stringN_of_int (k1) (n div 10) ^ Int.toString (n mod 10); 

15610  141 

15347  142 
fun ascii_of_c c = 
15610  143 
if Char.isAlphaNum c then String.str c 
144 
else if c = #"_" then "__" 

24310  145 
else if #" " <= c andalso c <= #"/" 
15610  146 
then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) 
24310  147 
else if Char.isPrint c 
24183  148 
then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) 
15610  149 
else "" 
15347  150 

15610  151 
val ascii_of = String.translate ascii_of_c; 
152 

24183  153 
(** Remove ASCII armouring from names in proof files **) 
154 

155 
(*We don't raise error exceptions because this code can run inside the watcher. 

156 
Also, the errors are "impossible" (hah!)*) 

157 
fun undo_ascii_aux rcs [] = String.implode(rev rcs) 

158 
 undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*) 

159 
(*Three types of _ escapes: __, _A to _P, _nnn*) 

160 
 undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs 

24310  161 
 undo_ascii_aux rcs (#"_" :: c :: cs) = 
24183  162 
if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*) 
163 
then undo_ascii_aux (Char.chr(Char.ord c  A_minus_space) :: rcs) cs 

24310  164 
else 
24183  165 
let val digits = List.take (c::cs, 3) handle Subscript => [] 
24310  166 
in 
24183  167 
case Int.fromString (String.implode digits) of 
168 
NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*) 

169 
 SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) 

170 
end 

171 
 undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs; 

172 

173 
val undo_ascii_of = undo_ascii_aux [] o String.explode; 

15347  174 

17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

175 
(* convert a list of strings into one single string; surrounded by brackets *) 
18218
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

176 
fun paren_pack [] = "" (*empty argument list*) 
9a7ffce389c3
new treatment of polymorphic types, using Sign.const_typargs
paulson
parents:
18199
diff
changeset

177 
 paren_pack strings = "(" ^ commas strings ^ ")"; 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

178 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

179 
fun tptp_clause strings = "(" ^ space_implode "  " strings ^ ")" 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

180 

16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

181 
(*Remove the initial ' character from a type variable, if it is present*) 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

182 
fun trim_type_var s = 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

183 
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

184 
else error ("trim_type: Malformed type variable encountered: " ^ s); 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

185 

16903  186 
fun ascii_of_indexname (v,0) = ascii_of v 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

187 
 ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; 
15347  188 

17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

189 
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); 
15347  190 
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); 
191 

24310  192 
fun make_schematic_type_var (x,i) = 
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

193 
tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); 
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset

194 
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); 
15347  195 

36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36476
diff
changeset

196 
val max_dfg_symbol_length = 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36476
diff
changeset

197 
if is_new_spass_version then 1000000 (* arbitrary large number *) else 63 
36378  198 

199 
(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *) 

36062  200 
fun controlled_length dfg s = 
36378  201 
if dfg andalso size s > max_dfg_symbol_length then 
202 
String.extract (s, 0, SOME (max_dfg_symbol_length div 2  1)) ^ "__" ^ 

203 
String.extract (s, size s  max_dfg_symbol_length div 2 + 1, NONE) 

204 
else 

205 
s 

23075  206 

30151  207 
fun lookup_const dfg c = 
17412  208 
case Symtab.lookup const_trans_table c of 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

209 
SOME c' => c' 
30151  210 
 NONE => controlled_length dfg (ascii_of c); 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

211 

30151  212 
fun lookup_type_const dfg c = 
17412  213 
case Symtab.lookup type_const_trans_table c of 
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset

214 
SOME c' => c' 
30151  215 
 NONE => controlled_length dfg (ascii_of c); 
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

216 

36062  217 
(* "op =" MUST BE "equal" because it's built into ATPs. *) 
218 
fun make_fixed_const _ (@{const_name "op ="}) = "equal" 

219 
 make_fixed_const dfg c = const_prefix ^ lookup_const dfg c; 

18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

220 

30151  221 
fun make_fixed_type_const dfg c = tconst_prefix ^ lookup_type_const dfg c; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

222 

17261  223 
fun make_type_class clas = class_prefix ^ ascii_of clas; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

224 

ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

225 

36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

226 
(**** name pool ****) 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

227 

27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

228 
type name = string * string 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

229 
type name_pool = string Symtab.table * string Symtab.table 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

230 

36222
0e3e49bd658d
don't use readable names if proof reconstruction is needed, because it uses the structure of names
blanchet
parents:
36221
diff
changeset

231 
fun empty_name_pool readable_names = 
0e3e49bd658d
don't use readable names if proof reconstruction is needed, because it uses the structure of names
blanchet
parents:
36221
diff
changeset

232 
if readable_names then SOME (`I Symtab.empty) else NONE 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

233 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

234 
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

235 
fun pool_map f xs = 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

236 
pool_fold (fn x => fn ys => fn pool => f x pool >> (fn y => y :: ys)) xs [] 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

237 

27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

238 
fun add_nice_name full_name nice_prefix j the_pool = 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

239 
let 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

240 
val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j) 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

241 
in 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

242 
case Symtab.lookup (snd the_pool) nice_name of 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

243 
SOME full_name' => 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

244 
if full_name = full_name' then (nice_name, the_pool) 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

245 
else add_nice_name full_name nice_prefix (j + 1) the_pool 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

246 
 NONE => 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

247 
(nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool), 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

248 
Symtab.update_new (nice_name, full_name) (snd the_pool))) 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

249 
end 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

250 

27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

251 
fun translate_first_char f s = 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

252 
String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE) 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

253 

36222
0e3e49bd658d
don't use readable names if proof reconstruction is needed, because it uses the structure of names
blanchet
parents:
36221
diff
changeset

254 
fun readable_name full_name s = 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

255 
let 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

256 
val s = s > Long_Name.base_name 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

257 
> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"] 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

258 
val s' = s > explode > rev > dropwhile (curry (op =) "'") 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

259 
val s' = 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

260 
(s' > rev 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

261 
> implode 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

262 
> String.translate 
36221  263 
(fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c 
264 
else "")) 

36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

265 
^ replicate_string (String.size s  length s') "_" 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

266 
val s' = 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

267 
if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s' 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

268 
else s' 
36476
a04cf4704668
in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
blanchet
parents:
36393
diff
changeset

269 
(* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous 
a04cf4704668
in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
blanchet
parents:
36393
diff
changeset

270 
("op &", "op ", etc.). *) 
a04cf4704668
in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
blanchet
parents:
36393
diff
changeset

271 
val s' = if s' = "equal" orelse s' = "op" then full_name else s' 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

272 
in 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

273 
case (Char.isLower (String.sub (full_name, 0)), 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

274 
Char.isLower (String.sub (s', 0))) of 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

275 
(true, false) => translate_first_char Char.toLower s' 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

276 
 (false, true) => translate_first_char Char.toUpper s' 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

277 
 _ => s' 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

278 
end 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

279 

27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

280 
fun nice_name (full_name, _) NONE = (full_name, NONE) 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

281 
 nice_name (full_name, desired_name) (SOME the_pool) = 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

282 
case Symtab.lookup (fst the_pool) full_name of 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

283 
SOME nice_name => (nice_name, SOME the_pool) 
36222
0e3e49bd658d
don't use readable names if proof reconstruction is needed, because it uses the structure of names
blanchet
parents:
36221
diff
changeset

284 
 NONE => add_nice_name full_name (readable_name full_name desired_name) 0 
0e3e49bd658d
don't use readable names if proof reconstruction is needed, because it uses the structure of names
blanchet
parents:
36221
diff
changeset

285 
the_pool 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

286 
> apsnd SOME 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

287 

27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

288 
(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

289 
format ****) 
15347  290 

21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

291 
datatype kind = Axiom  Conjecture; 
23385  292 

15347  293 
type axiom_name = string; 
294 

295 
(**** Isabelle FOL clauses ****) 

296 

36168
0a6ed065683d
give more sensible names to "fol_type" constructors, as requested by a FIXME comment
blanchet
parents:
36167
diff
changeset

297 
datatype fol_type = 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

298 
TyVar of name  
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

299 
TyFree of name  
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

300 
TyConstr of name * fol_type list 
18402
aaba095cf62b
1. changed fol_type, it's not a string type anymore.
mengj
parents:
18390
diff
changeset

301 

36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

302 
fun string_of_fol_type (TyVar sp) pool = nice_name sp pool 
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

303 
 string_of_fol_type (TyFree sp) pool = nice_name sp pool 
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

304 
 string_of_fol_type (TyConstr (sp, tys)) pool = 
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

305 
let 
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

306 
val (s, pool) = nice_name sp pool 
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

307 
val (ss, pool) = pool_map string_of_fol_type tys pool 
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

308 
in (s ^ paren_pack ss, pool) end 
24310  309 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

310 
(* The first component is the type class; the second is a TVar or TFree. *) 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

311 
datatype type_literal = 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

312 
TyLitVar of string * name  
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

313 
TyLitFree of string * name 
15347  314 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset

315 
exception CLAUSE of string * term; 
15347  316 

24310  317 
(*Make literals for sorted type variables*) 
24940  318 
fun sorts_on_typs_aux (_, []) = [] 
319 
 sorts_on_typs_aux ((x,i), s::ss) = 

320 
let val sorts = sorts_on_typs_aux ((x,i), ss) 

22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

321 
in 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

322 
if s = "HOL.type" then sorts 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

323 
else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

324 
else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts 
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

325 
end; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

326 

24940  327 
fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s) 
328 
 sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s); 

329 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

330 
fun pred_of_sort (TyLitVar (s, _)) = (s, 1) 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

331 
 pred_of_sort (TyLitFree (s, _)) = (s, 1) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

332 

24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

333 
(*Given a list of sorted type variables, return a list of type literals.*) 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

334 
fun add_type_literals Ts = fold (union (op =)) (map sorts_on_typs Ts) [] 
20015
1ffcf4802802
Literals aren't sorted any more. Output overloaded constants' type var instantiations.
mengj
parents:
19719
diff
changeset

335 

29676  336 
(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear. 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

337 
* Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a 
29676  338 
in a lemma has the same sort as 'a in the conjecture. 
339 
* Deleting such clauses will lead to problems with locales in other use of local results 

340 
where 'a is fixed. Probably we should delete clauses unless the sorts agree. 

341 
* Currently we include a class constraint in the clause, exactly as with TVars. 

342 
*) 

343 

20015
1ffcf4802802
Literals aren't sorted any more. Output overloaded constants' type var instantiations.
mengj
parents:
19719
diff
changeset

344 
(** make axiom and conjecture clauses. **) 
1ffcf4802802
Literals aren't sorted any more. Output overloaded constants' type var instantiations.
mengj
parents:
19719
diff
changeset

345 

1ffcf4802802
Literals aren't sorted any more. Output overloaded constants' type var instantiations.
mengj
parents:
19719
diff
changeset

346 
fun get_tvar_strs [] = [] 
24940  347 
 get_tvar_strs ((TVar (indx,s))::Ts) = 
348 
insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts) 

349 
 get_tvar_strs((TFree _)::Ts) = get_tvar_strs Ts 

20015
1ffcf4802802
Literals aren't sorted any more. Output overloaded constants' type var instantiations.
mengj
parents:
19719
diff
changeset

350 

24310  351 

19354  352 

15347  353 
(**** Isabelle arities ****) 
354 

24310  355 
datatype arLit = TConsLit of class * string * string list 
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

356 
 TVarLit of class * string; 
24310  357 

35865  358 
datatype arity_clause = 
24310  359 
ArityClause of {axiom_name: axiom_name, 
360 
conclLit: arLit, 

361 
premLits: arLit list}; 

15347  362 

363 

18798  364 
fun gen_TVars 0 = [] 
365 
 gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n1); 

15347  366 

18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

367 
fun pack_sort(_,[]) = [] 
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

368 
 pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*) 
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

369 
 pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt); 
24310  370 

18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset

371 
(*Arity of type constructor tcon :: (arg1,...,argN)res*) 
30151  372 
fun make_axiom_arity_clause dfg (tcons, axiom_name, (cls,args)) = 
21560  373 
let val tvars = gen_TVars (length args) 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

374 
val tvars_srts = ListPair.zip (tvars,args) 
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

375 
in 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

376 
ArityClause {axiom_name = axiom_name, 
30151  377 
conclLit = TConsLit (cls, make_fixed_type_const dfg tcons, tvars), 
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

378 
premLits = map TVarLit (union_all(map pack_sort tvars_srts))} 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

379 
end; 
15347  380 

381 

382 
(**** Isabelle class relations ****) 

383 

35865  384 
datatype classrel_clause = 
24310  385 
ClassrelClause of {axiom_name: axiom_name, 
386 
subclass: class, 

387 
superclass: class}; 

388 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset

389 
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) 
21432
625797c592b2
Optimized class_pairs for the common case of no subclasses
paulson
parents:
21416
diff
changeset

390 
fun class_pairs thy [] supers = [] 
625797c592b2
Optimized class_pairs for the common case of no subclasses
paulson
parents:
21416
diff
changeset

391 
 class_pairs thy subs supers = 
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

392 
let 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

393 
val class_less = Sorts.class_less (Sign.classes_of thy) 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

394 
fun add_super sub super = class_less (sub, super) ? cons (sub, super) 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

395 
fun add_supers sub = fold (add_super sub) supers 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

396 
in fold add_supers subs [] end 
15347  397 

35865  398 
fun make_classrel_clause (sub,super) = 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset

399 
ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super, 
24310  400 
subclass = make_type_class sub, 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset

401 
superclass = make_type_class super}; 
15347  402 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset

403 
fun make_classrel_clauses thy subs supers = 
35865  404 
map make_classrel_clause (class_pairs thy subs supers); 
18868  405 

406 

407 
(** Isabelle arities **) 

17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

408 

30151  409 
fun arity_clause dfg _ _ (tcons, []) = [] 
410 
 arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) 

411 
arity_clause dfg seen n (tcons,ars) 

412 
 arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) = 

21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset

413 
if class mem_string seen then (*multiple arities for the same tycon, class pair*) 
30151  414 
make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: 
415 
arity_clause dfg seen (n+1) (tcons,ars) 

21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset

416 
else 
30151  417 
make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class, ar) :: 
418 
arity_clause dfg (class::seen) n (tcons,ars) 

17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

419 

30151  420 
fun multi_arity_clause dfg [] = [] 
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

421 
 multi_arity_clause dfg ((tcons, ars) :: tc_arlists) = 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

422 
arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

423 

22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

424 
(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

425 
provided its arguments have the corresponding sorts.*) 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset

426 
fun type_class_pairs thy tycons classes = 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset

427 
let val alg = Sign.classes_of thy 
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

428 
fun domain_sorts tycon = Sorts.mg_domain alg tycon o single 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

429 
fun add_class tycon class = 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

430 
cons (class, domain_sorts tycon class) 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

431 
handle Sorts.CLASS_ERROR _ => I 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

432 
fun try_classes tycon = (tycon, fold (add_class tycon) classes []) 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset

433 
in map try_classes tycons end; 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset

434 

22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

435 
(*Proving one (tycon, class) membership may require proving others, so iterate.*) 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

436 
fun iter_type_class_pairs thy tycons [] = ([], []) 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

437 
 iter_type_class_pairs thy tycons classes = 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

438 
let val cpairs = type_class_pairs thy tycons classes 
33040  439 
val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) 
440 
> subtract (op =) classes > subtract (op =) HOLogic.typeS 

24310  441 
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses 
33042  442 
in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; 
24310  443 

30151  444 
fun make_arity_clauses_dfg dfg thy tycons classes = 
24310  445 
let val (classes', cpairs) = iter_type_class_pairs thy tycons classes 
30151  446 
in (classes', multi_arity_clause dfg cpairs) end; 
447 
val make_arity_clauses = make_arity_clauses_dfg false; 

17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

448 

18868  449 
(**** Find occurrences of predicates in clauses ****) 
450 

24310  451 
(*FIXME: multiplearity checking doesn't work, as update_new is the wrong 
18868  452 
function (it flags repeated declarations of a function, even with the same arity)*) 
453 

36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

454 
fun update_many keypairs = fold Symtab.update keypairs 
18868  455 

36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

456 
val add_type_sort_preds = update_many o map pred_of_sort o sorts_on_typs 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

457 

36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

458 
fun add_classrel_clause_preds (ClassrelClause {subclass, superclass, ...}) = 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

459 
Symtab.update (subclass, 1) #> Symtab.update (superclass, 1) 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

460 

22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

461 
fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

462 
 class_of_arityLit (TVarLit (tclass, _)) = tclass; 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset

463 

36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

464 
fun add_arity_clause_preds (ArityClause {conclLit, premLits, ...}) = 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

465 
let 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

466 
val classes = map (make_type_class o class_of_arityLit) 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

467 
(conclLit :: premLits) 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

468 
in fold (Symtab.update o rpair 1) classes end; 
18868  469 

470 
(*** Find occurrences of functions in clauses ***) 

471 

36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

472 
fun add_fol_type_funcs (TyVar _) = I 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

473 
 add_fol_type_funcs (TyFree (s, _)) = Symtab.update (s, 0) 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

474 
 add_fol_type_funcs (TyConstr ((s, _), tys)) = 
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

475 
Symtab.update (s, length tys) #> fold add_fol_type_funcs tys 
18868  476 

20038  477 
(*TFrees are recorded as constants*) 
24940  478 
fun add_type_sort_funcs (TVar _, funcs) = funcs 
479 
 add_type_sort_funcs (TFree (a, _), funcs) = 

20038  480 
Symtab.update (make_fixed_type_var a, 0) funcs 
481 

36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset

482 
fun add_arity_clause_funcs (ArityClause {conclLit,...}) funcs = 
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

483 
let val TConsLit (_, tcons, tvars) = conclLit 
18868  484 
in Symtab.update (tcons, length tvars) funcs end; 
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset

485 

23075  486 
(*This type can be overlooked because it is builtin...*) 
487 
val init_functab = Symtab.update ("tc_itself", 1) Symtab.empty; 

488 

18868  489 

490 
(**** Stringoriented operations ****) 

15347  491 

24310  492 
fun string_of_clausename (cls_id,ax_name) = 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

493 
clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id; 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17312
diff
changeset

494 

24310  495 
fun string_of_type_clsname (cls_id,ax_name,idx) = 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

496 
string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); 
18863  497 

24310  498 

18868  499 
(**** Producing DFG files ****) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

500 

18863  501 
(*Attach sign in DFG syntax: false means negate.*) 
502 
fun dfg_sign true s = s 

24310  503 
 dfg_sign false s = "not(" ^ s ^ ")" 
18863  504 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

505 
fun dfg_of_type_literal pos (TyLitVar (s, (s', _))) = 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

506 
dfg_sign pos (s ^ "(" ^ s' ^ ")") 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

507 
 dfg_of_type_literal pos (TyLitFree (s, (s', _))) = 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

508 
dfg_sign pos (s ^ "(" ^ s' ^ ")"); 
24310  509 

18868  510 
(*Enclose the clause body by quantifiers, if necessary*) 
24310  511 
fun dfg_forall [] body = body 
18868  512 
 dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")" 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

513 

24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

514 
fun gen_dfg_cls (cls_id, ax_name, Axiom, lits, tylits, vars) = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

515 
"clause( %(axiom)\n" ^ 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

516 
dfg_forall vars ("or(" ^ commas (tylits@lits) ^ ")") ^ ",\n" ^ 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

517 
string_of_clausename (cls_id,ax_name) ^ ").\n\n" 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

518 
 gen_dfg_cls (cls_id, ax_name, Conjecture, lits, _, vars) = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

519 
"clause( %(negated_conjecture)\n" ^ 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

520 
dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^ 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

521 
string_of_clausename (cls_id,ax_name) ^ ").\n\n"; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

522 

18798  523 
fun string_of_arity (name, num) = "(" ^ name ^ "," ^ Int.toString num ^ ")" 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

524 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

525 
fun string_of_preds [] = "" 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

526 
 string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n"; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

527 

18856
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

528 
fun string_of_funcs [] = "" 
4669dec681f4
tidyup of res_clause.ML, removing the "predicates" field
paulson
parents:
18798
diff
changeset

529 
 string_of_funcs funcs = "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

530 

24310  531 
fun string_of_symbols predstr funcstr = 
17234  532 
"list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n"; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

533 

18798  534 
fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n"; 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

535 

24310  536 
fun string_of_descrip name = 
537 
"list_of_descriptions.\nname({*" ^ name ^ 

18868  538 
"*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*autogenerated*}).\nend_of_list.\n\n" 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

539 

18863  540 
fun dfg_tfree_clause tfree_lit = 
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

541 
"clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n" 
18863  542 

22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

543 
fun dfg_of_arLit (TConsLit (c,t,args)) = 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

544 
dfg_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")") 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

545 
 dfg_of_arLit (TVarLit (c,str)) = 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

546 
dfg_sign false (make_type_class c ^ "(" ^ str ^ ")") 
24310  547 

20038  548 
fun dfg_classrelLits sub sup = "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)"; 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset

549 

35865  550 
fun dfg_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) = 
18868  551 
"clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^ 
552 
axiom_name ^ ").\n\n"; 

24310  553 

21560  554 
fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name; 
555 

24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

556 
fun dfg_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) = 
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

557 
let val TConsLit (_,_,tvars) = conclLit 
18868  558 
val lits = map dfg_of_arLit (conclLit :: premLits) 
18863  559 
in 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

560 
"clause( %(axiom)\n" ^ 
18868  561 
dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^ 
21560  562 
string_of_ar axiom_name ^ ").\n\n" 
18863  563 
end; 
564 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

565 

18869
00741f7280f7
removal of ResClause.num_of_clauses and other simplifications
paulson
parents:
18868
diff
changeset

566 
(**** Produce TPTP files ****) 
18868  567 

21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

568 
fun tptp_sign true s = s 
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

569 
 tptp_sign false s = "~ " ^ s 
18868  570 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

571 
fun tptp_of_type_literal pos (TyLitVar (s, name)) = 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

572 
nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")")) 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

573 
 tptp_of_type_literal pos (TyLitFree (s, name)) = 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

574 
nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")")) 
36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36063
diff
changeset

575 

c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36063
diff
changeset

576 
fun tptp_cnf name kind formula = 
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36063
diff
changeset

577 
"cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n" 
24310  578 

36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36063
diff
changeset

579 
fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) = 
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36063
diff
changeset

580 
tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom" 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

581 
(tptp_clause (tylits @ lits)) 
36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36063
diff
changeset

582 
 gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) = 
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36063
diff
changeset

583 
tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture" 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

584 
(tptp_clause lits) 
15347  585 

18863  586 
fun tptp_tfree_clause tfree_lit = 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

587 
tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_clause [tfree_lit]) 
24310  588 

22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

589 
fun tptp_of_arLit (TConsLit (c,t,args)) = 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

590 
tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")") 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

591 
 tptp_of_arLit (TVarLit (c,str)) = 
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset

592 
tptp_sign false (make_type_class c ^ "(" ^ str ^ ")") 
24310  593 

24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset

594 
fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) = 
36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36063
diff
changeset

595 
tptp_cnf (string_of_ar axiom_name) "axiom" 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

596 
(tptp_clause (map tptp_of_arLit (conclLit :: premLits))) 
15347  597 

24310  598 
fun tptp_classrelLits sub sup = 
21509
6c5755ad9cae
ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents:
21470
diff
changeset

599 
let val tvar = "(T)" 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36493
diff
changeset

600 
in tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end; 
15347  601 

35865  602 
fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) = 
36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36063
diff
changeset

603 
tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass) 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

604 

15347  605 
end; 