author  blanchet 
Tue, 20 Mar 2012 18:42:45 +0100  
changeset 47054  b86864a2b16e 
parent 47053  7585d0120f1d 
child 47073  c73f7b0c7ebc 
permissions  rwrr 
38047  1 
(* Title: HOL/Tools/ATP/atp_problem.ML 
38027  2 
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA 
37509
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 

39452  5 
Abstract representation of ATP problems and TPTP syntax. 
37509
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 

38019
e207a64e1e0b
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
blanchet
parents:
38018
diff
changeset

8 
signature ATP_PROBLEM = 
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset

9 
sig 
43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43422
diff
changeset

10 
datatype ('a, 'b) ho_term = 
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43422
diff
changeset

11 
ATerm of 'a * ('a, 'b) ho_term list  
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43422
diff
changeset

12 
AAbs of ('a * 'b) * ('a, 'b) ho_term 
37992  13 
datatype quantifier = AForall  AExists 
43163  14 
datatype connective = ANot  AAnd  AOr  AImplies  AIff 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

15 
datatype ('a, 'b, 'c) formula = 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

16 
AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula  
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

17 
AConn of connective * ('a, 'b, 'c) formula list  
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

18 
AAtom of 'c 
37994
b04307085a09
make TPTP generator accept full firstorder formulas
blanchet
parents:
37993
diff
changeset

19 

44593
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

20 
datatype 'a ho_type = 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

21 
AType of 'a * 'a ho_type list  
44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

22 
AFun of 'a ho_type * 'a ho_type  
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

23 
ATyAbs of 'a list * 'a ho_type 
42963  24 

47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

25 
type term_order = 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

26 
{is_lpo : bool, 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

27 
gen_weights : bool, 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

28 
gen_prec : bool, 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

29 
gen_simp : bool} 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

30 

44754  31 
datatype tptp_polymorphism = TPTP_Monomorphic  TPTP_Polymorphic 
32 
datatype tptp_explicitness = TPTP_Implicit  TPTP_Explicit 

44589
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44501
diff
changeset

33 
datatype thf_flavor = THF_Without_Choice  THF_With_Choice 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

34 
datatype dfg_flavor = DFG_Unsorted  DFG_Sorted 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

35 

866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

36 
datatype atp_format = 
44235
85e9dad3c187
distinguish THF syntax with and without choice (Satallax vs. LEOII)
blanchet
parents:
43987
diff
changeset

37 
CNF  
85e9dad3c187
distinguish THF syntax with and without choice (Satallax vs. LEOII)
blanchet
parents:
43987
diff
changeset

38 
CNF_UEQ  
85e9dad3c187
distinguish THF syntax with and without choice (Satallax vs. LEOII)
blanchet
parents:
43987
diff
changeset

39 
FOF  
44754  40 
TFF of tptp_polymorphism * tptp_explicitness  
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

41 
THF of tptp_polymorphism * tptp_explicitness * thf_flavor  
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

42 
DFG of dfg_flavor 
44235
85e9dad3c187
distinguish THF syntax with and without choice (Satallax vs. LEOII)
blanchet
parents:
43987
diff
changeset

43 

42525
7a506b0b644f
distinguish FOF and TFF (typed firstorder) in ATP abstract syntax tree
blanchet
parents:
42449
diff
changeset

44 
datatype formula_kind = Axiom  Definition  Lemma  Hypothesis  Conjecture 
42527
6a9458524f01
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents:
42526
diff
changeset

45 
datatype 'a problem_line = 
42963  46 
Decl of string * 'a * 'a ho_type  
44402  47 
Formula of string * formula_kind 
48 
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula 

49 
* (string, string ho_type) ho_term option 

46406  50 
* (string, string ho_type) ho_term list 
38017
3ad3e3ca2451
move Sledgehammerspecific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38014
diff
changeset

51 
type 'a problem = (string * 'a problem_line list) list 
37992  52 

42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

53 
val tptp_cnf : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

54 
val tptp_fof : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

55 
val tptp_tff : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

56 
val tptp_thf : string 
42967  57 
val tptp_has_type : string 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

58 
val tptp_type_of_types : string 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

59 
val tptp_bool_type : string 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

60 
val tptp_individual_type : string 
42963  61 
val tptp_fun_type : string 
42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

62 
val tptp_product_type : string 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

63 
val tptp_forall : string 
43678  64 
val tptp_ho_forall : string 
44650  65 
val tptp_pi_binder : string 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

66 
val tptp_exists : string 
43678  67 
val tptp_ho_exists : string 
44495  68 
val tptp_choice : string 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

69 
val tptp_not : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

70 
val tptp_and : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

71 
val tptp_or : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

72 
val tptp_implies : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

73 
val tptp_if : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

74 
val tptp_iff : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

75 
val tptp_not_iff : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

76 
val tptp_app : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

77 
val tptp_not_infix : string 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

78 
val tptp_equal : string 
43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

79 
val tptp_old_equal : string 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

80 
val tptp_false : string 
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

81 
val tptp_true : string 
43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

82 
val tptp_empty_list : string 
46406  83 
val isabelle_info_prefix : string 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

84 
val isabelle_info : string > int > (string, 'a) ho_term list 
46442
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

85 
val extract_isabelle_status : (string, 'a) ho_term list > string option 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

86 
val extract_isabelle_rank : (string, 'a) ho_term list > int 
46406  87 
val introN : string 
88 
val elimN : string 

89 
val simpN : string 

90 
val spec_eqN : string 

91 
val rankN : string 

92 
val minimum_rank : int 

93 
val default_rank : int 

47030  94 
val default_term_order_weight : int 
43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

95 
val is_tptp_equal : string > bool 
42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

96 
val is_built_in_tptp_symbol : string > bool 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

97 
val is_tptp_variable : string > bool 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

98 
val is_tptp_user_symbol : string > bool 
44595
444d111bde7d
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
blanchet
parents:
44594
diff
changeset

99 
val atype_of_types : (string * string) ho_type 
444d111bde7d
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
blanchet
parents:
44594
diff
changeset

100 
val bool_atype : (string * string) ho_type 
444d111bde7d
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
blanchet
parents:
44594
diff
changeset

101 
val individual_atype : (string * string) ho_type 
42942  102 
val mk_anot : ('a, 'b, 'c) formula > ('a, 'b, 'c) formula 
103 
val mk_aconn : 

104 
connective > ('a, 'b, 'c) formula > ('a, 'b, 'c) formula 

105 
> ('a, 'b, 'c) formula 

42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

106 
val aconn_fold : 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

107 
bool option > (bool option > 'a > 'b > 'b) > connective * 'a list 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

108 
> 'b > 'b 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

109 
val aconn_map : 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

110 
bool option > (bool option > 'a > ('b, 'c, 'd) formula) 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

111 
> connective * 'a list > ('b, 'c, 'd) formula 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

112 
val formula_fold : 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

113 
bool option > (bool option > 'c > 'd > 'd) > ('a, 'b, 'c) formula 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

114 
> 'd > 'd 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42942
diff
changeset

115 
val formula_map : ('c > 'd) > ('a, 'b, 'c) formula > ('a, 'b, 'd) formula 
46442
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

116 
val is_function_type : string ho_type > bool 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

117 
val is_predicate_type : string ho_type > bool 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

118 
val is_format_higher_order : atp_format > bool 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

119 
val is_format_typed : atp_format > bool 
46442
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

120 
val lines_for_atp_problem : 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

121 
atp_format > term_order > (unit > (string * int) list) > string problem 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

122 
> string list 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43085
diff
changeset

123 
val ensure_cnf_problem : 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43085
diff
changeset

124 
(string * string) problem > (string * string) problem 
42939  125 
val filter_cnf_ueq_problem : 
126 
(string * string) problem > (string * string) problem 

45828
3b8606fba2dd
correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
blanchet
parents:
45304
diff
changeset

127 
val declared_syms_in_problem : (string * ''a) problem > (string * ''a) list 
39452  128 
val nice_atp_problem : 
45939
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

129 
bool > atp_format > ('a * (string * string) problem_line list) list 
38017
3ad3e3ca2451
move Sledgehammerspecific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38014
diff
changeset

130 
> ('a * string problem_line list) list 
3ad3e3ca2451
move Sledgehammerspecific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38014
diff
changeset

131 
* (string Symtab.table * string Symtab.table) option 
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset

132 
end; 
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset

133 

38019
e207a64e1e0b
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
blanchet
parents:
38018
diff
changeset

134 
structure ATP_Problem : ATP_PROBLEM = 
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset

135 
struct 
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset

136 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43000
diff
changeset

137 
open ATP_Util 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43000
diff
changeset

138 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43000
diff
changeset

139 

37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset

140 
(** ATP problem **) 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset

141 

43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43422
diff
changeset

142 
datatype ('a, 'b) ho_term = 
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43422
diff
changeset

143 
ATerm of 'a * ('a, 'b) ho_term list  
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43422
diff
changeset

144 
AAbs of ('a * 'b) * ('a, 'b) ho_term 
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset

145 
datatype quantifier = AForall  AExists 
43163  146 
datatype connective = ANot  AAnd  AOr  AImplies  AIff 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

147 
datatype ('a, 'b, 'c) formula = 
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

148 
AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula  
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

149 
AConn of connective * ('a, 'b, 'c) formula list  
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

150 
AAtom of 'c 
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset

151 

44593
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

152 
datatype 'a ho_type = 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

153 
AType of 'a * 'a ho_type list  
44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

154 
AFun of 'a ho_type * 'a ho_type  
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

155 
ATyAbs of 'a list * 'a ho_type 
42963  156 

47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

157 
type term_order = 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

158 
{is_lpo : bool, 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

159 
gen_weights : bool, 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

160 
gen_prec : bool, 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

161 
gen_simp : bool} 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

162 

44754  163 
datatype tptp_polymorphism = TPTP_Monomorphic  TPTP_Polymorphic 
164 
datatype tptp_explicitness = TPTP_Implicit  TPTP_Explicit 

44589
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44501
diff
changeset

165 
datatype thf_flavor = THF_Without_Choice  THF_With_Choice 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

166 
datatype dfg_flavor = DFG_Unsorted  DFG_Sorted 
44499  167 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

168 
datatype atp_format = 
44235
85e9dad3c187
distinguish THF syntax with and without choice (Satallax vs. LEOII)
blanchet
parents:
43987
diff
changeset

169 
CNF  
85e9dad3c187
distinguish THF syntax with and without choice (Satallax vs. LEOII)
blanchet
parents:
43987
diff
changeset

170 
CNF_UEQ  
85e9dad3c187
distinguish THF syntax with and without choice (Satallax vs. LEOII)
blanchet
parents:
43987
diff
changeset

171 
FOF  
44754  172 
TFF of tptp_polymorphism * tptp_explicitness  
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

173 
THF of tptp_polymorphism * tptp_explicitness * thf_flavor  
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

174 
DFG of dfg_flavor 
44235
85e9dad3c187
distinguish THF syntax with and without choice (Satallax vs. LEOII)
blanchet
parents:
43987
diff
changeset

175 

42525
7a506b0b644f
distinguish FOF and TFF (typed firstorder) in ATP abstract syntax tree
blanchet
parents:
42449
diff
changeset

176 
datatype formula_kind = Axiom  Definition  Lemma  Hypothesis  Conjecture 
42527
6a9458524f01
reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents:
42526
diff
changeset

177 
datatype 'a problem_line = 
42963  178 
Decl of string * 'a * 'a ho_type  
46406  179 
Formula of string * formula_kind 
180 
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula 

181 
* (string, string ho_type) ho_term option 

182 
* (string, string ho_type) ho_term list 

37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset

183 
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

184 

42722  185 
(* official TPTP syntax *) 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

186 
val tptp_cnf = "cnf" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

187 
val tptp_fof = "fof" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

188 
val tptp_tff = "tff" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

189 
val tptp_thf = "thf" 
42967  190 
val tptp_has_type = ":" 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

191 
val tptp_type_of_types = "$tType" 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

192 
val tptp_bool_type = "$o" 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

193 
val tptp_individual_type = "$i" 
42963  194 
val tptp_fun_type = ">" 
42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

195 
val tptp_product_type = "*" 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

196 
val tptp_forall = "!" 
43678  197 
val tptp_ho_forall = "!!" 
44650  198 
val tptp_pi_binder = "!>" 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

199 
val tptp_exists = "?" 
43678  200 
val tptp_ho_exists = "??" 
44495  201 
val tptp_choice = "@+" 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

202 
val tptp_not = "~" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

203 
val tptp_and = "&" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

204 
val tptp_or = "" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

205 
val tptp_implies = "=>" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

206 
val tptp_if = "<=" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

207 
val tptp_iff = "<=>" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

208 
val tptp_not_iff = "<~>" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

209 
val tptp_app = "@" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

210 
val tptp_not_infix = "!" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

211 
val tptp_equal = "=" 
43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

212 
val tptp_old_equal = "equal" 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

213 
val tptp_false = "$false" 
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

214 
val tptp_true = "$true" 
43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

215 
val tptp_empty_list = "[]" 
42722  216 

46406  217 
val isabelle_info_prefix = "isabelle_" 
218 

219 
val introN = "intro" 

220 
val elimN = "elim" 

221 
val simpN = "simp" 

222 
val spec_eqN = "spec_eq" 

223 
val rankN = "rank" 

224 

225 
val minimum_rank = 0 

226 
val default_rank = 1000 

47030  227 
val default_term_order_weight = 1 
46406  228 

229 
(* Currently, only newer versions of SPASS, with sorted DFG format support, can 

230 
process Isabelle metainformation. *) 

47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

231 
fun isabelle_info status rank = 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

232 
[] > rank <> default_rank 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

233 
? cons (ATerm (isabelle_info_prefix ^ rankN, 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

234 
[ATerm (string_of_int rank, [])])) 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

235 
> status <> "" ? cons (ATerm (isabelle_info_prefix ^ status, [])) 
46406  236 

237 
fun extract_isabelle_status (ATerm (s, []) :: _) = 

238 
try (unprefix isabelle_info_prefix) s 

239 
 extract_isabelle_status _ = NONE 

240 

241 
fun extract_isabelle_rank (tms as _ :: _) = 

242 
(case List.last tms of 

243 
ATerm (_, [ATerm (rank, [])]) => the (Int.fromString rank) 

244 
 _ => default_rank) 

245 
 extract_isabelle_rank _ = default_rank 

246 

43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

247 
fun is_tptp_equal s = (s = tptp_equal orelse s = tptp_old_equal) 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

248 
fun is_built_in_tptp_symbol s = 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

249 
s = tptp_old_equal orelse not (Char.isAlpha (String.sub (s, 0))) 
42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

250 
fun is_tptp_variable s = Char.isUpper (String.sub (s, 0)) 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

251 
val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol) 
42939  252 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

253 
val atype_of_types = AType (`I tptp_type_of_types, []) 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

254 
val bool_atype = AType (`I tptp_bool_type, []) 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

255 
val individual_atype = AType (`I tptp_individual_type, []) 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

256 

43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

257 
fun raw_polarities_of_conn ANot = (SOME false, NONE) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

258 
 raw_polarities_of_conn AAnd = (SOME true, SOME true) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

259 
 raw_polarities_of_conn AOr = (SOME true, SOME true) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

260 
 raw_polarities_of_conn AImplies = (SOME false, SOME true) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

261 
 raw_polarities_of_conn AIff = (NONE, NONE) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

262 
fun polarities_of_conn NONE = K (NONE, NONE) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

263 
 polarities_of_conn (SOME pos) = 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

264 
raw_polarities_of_conn #> not pos ? pairself (Option.map not) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

265 

42942  266 
fun mk_anot (AConn (ANot, [phi])) = phi 
267 
 mk_anot phi = AConn (ANot, [phi]) 

268 
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) 

269 

42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

270 
fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

271 
 aconn_fold pos f (AImplies, [phi1, phi2]) = 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

272 
f (Option.map not pos) phi1 #> f pos phi2 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

273 
 aconn_fold pos f (AAnd, phis) = fold (f pos) phis 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

274 
 aconn_fold pos f (AOr, phis) = fold (f pos) phis 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

275 
 aconn_fold _ f (_, phis) = fold (f NONE) phis 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

276 

1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

277 
fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi]) 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

278 
 aconn_map pos f (AImplies, [phi1, phi2]) = 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

279 
AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2]) 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

280 
 aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis) 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

281 
 aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis) 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

282 
 aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis) 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

283 

1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

284 
fun formula_fold pos f = 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

285 
let 
44501  286 
fun fld pos (AQuant (_, _, phi)) = fld pos phi 
287 
 fld pos (AConn conn) = aconn_fold pos fld conn 

288 
 fld pos (AAtom tm) = f pos tm 

289 
in fld pos end 

42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

290 

42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42942
diff
changeset

291 
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42942
diff
changeset

292 
 formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42942
diff
changeset

293 
 formula_map f (AAtom tm) = AAtom (f tm) 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42942
diff
changeset

294 

46442
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

295 
fun is_function_type (AFun (_, ty)) = is_function_type ty 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

296 
 is_function_type (AType (s, _)) = 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

297 
s <> tptp_type_of_types andalso s <> tptp_bool_type 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

298 
 is_function_type _ = false 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

299 
fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

300 
 is_predicate_type (AType (s, _)) = (s = tptp_bool_type) 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

301 
 is_predicate_type _ = false 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

302 
fun is_nontrivial_predicate_type (AFun (_, ty)) = is_predicate_type ty 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

303 
 is_nontrivial_predicate_type _ = false 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

304 

45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

305 
fun is_format_higher_order (THF _) = true 
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

306 
 is_format_higher_order _ = false 
44499  307 
fun is_format_typed (TFF _) = true 
44754  308 
 is_format_typed (THF _) = true 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

309 
 is_format_typed (DFG DFG_Sorted) = true 
44235
85e9dad3c187
distinguish THF syntax with and without choice (Satallax vs. LEOII)
blanchet
parents:
43987
diff
changeset

310 
 is_format_typed _ = false 
42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

311 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

312 
fun tptp_string_for_kind Axiom = "axiom" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

313 
 tptp_string_for_kind Definition = "definition" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

314 
 tptp_string_for_kind Lemma = "lemma" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

315 
 tptp_string_for_kind Hypothesis = "hypothesis" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

316 
 tptp_string_for_kind Conjecture = "conjecture" 
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38613
diff
changeset

317 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

318 
fun tptp_string_for_app format func args = 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

319 
if is_format_higher_order format then 
44787  320 
"(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")" 
321 
else 

322 
func ^ "(" ^ commas args ^ ")" 

323 

44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

324 
fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty) 
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

325 
 flatten_type (ty as AFun (ty1 as AType _, ty2)) = 
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

326 
(case flatten_type ty2 of 
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

327 
AFun (ty' as AType (s, tys), ty) => 
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

328 
AFun (AType (tptp_product_type, 
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

329 
ty1 :: (if s = tptp_product_type then tys else [ty'])), ty) 
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

330 
 _ => ty) 
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

331 
 flatten_type (ty as AType _) = ty 
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

332 
 flatten_type _ = 
42963  333 
raise Fail "unexpected higherorder type in firstorder format" 
334 

46445  335 
val dfg_individual_type = "iii" (* cannot clash *) 
46338
b02ff6b17599
better handling of individual type for DFG format (SPASS)
blanchet
parents:
46320
diff
changeset

336 

44787  337 
fun str_for_type format ty = 
44593
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

338 
let 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

339 
val dfg = (format = DFG DFG_Sorted) 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

340 
fun str _ (AType (s, [])) = 
46338
b02ff6b17599
better handling of individual type for DFG format (SPASS)
blanchet
parents:
46320
diff
changeset

341 
if dfg andalso s = tptp_individual_type then dfg_individual_type else s 
44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

342 
 str _ (AType (s, tys)) = 
44787  343 
let val ss = tys > map (str false) in 
344 
if s = tptp_product_type then 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

345 
ss > space_implode 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

346 
(if dfg then ", " else " " ^ tptp_product_type ^ " ") 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

347 
> (not dfg andalso length ss > 1) ? enclose "(" ")" 
44787  348 
else 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

349 
tptp_string_for_app format s ss 
44787  350 
end 
44593
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

351 
 str rhs (AFun (ty1, ty2)) = 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

352 
(str false ty1 > dfg ? enclose "(" ")") ^ " " ^ 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

353 
(if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2 
44593
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

354 
> not rhs ? enclose "(" ")" 
44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

355 
 str _ (ATyAbs (ss, ty)) = 
44650  356 
tptp_pi_binder ^ "[" ^ 
44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

357 
commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)) 
44739  358 
ss) ^ "]: " ^ str false ty 
44593
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

359 
in str true ty end 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

360 

44787  361 
fun string_for_type (format as THF _) ty = str_for_type format ty 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

362 
 string_for_type format ty = str_for_type format (flatten_type ty) 
42963  363 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

364 
fun tptp_string_for_quantifier AForall = tptp_forall 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

365 
 tptp_string_for_quantifier AExists = tptp_exists 
42963  366 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

367 
fun tptp_string_for_connective ANot = tptp_not 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

368 
 tptp_string_for_connective AAnd = tptp_and 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

369 
 tptp_string_for_connective AOr = tptp_or 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

370 
 tptp_string_for_connective AImplies = tptp_implies 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

371 
 tptp_string_for_connective AIff = tptp_iff 
42963  372 

42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

373 
fun string_for_bound_var format (s, ty) = 
44593
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

374 
s ^ 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

375 
(if is_format_typed format then 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

376 
" " ^ tptp_has_type ^ " " ^ 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

377 
(ty > the_default (AType (tptp_individual_type, [])) 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

378 
> string_for_type format) 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

379 
else 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44589
diff
changeset

380 
"") 
42963  381 

44754  382 
fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true 
383 
 is_format_with_choice _ = false 

384 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

385 
fun tptp_string_for_term _ (ATerm (s, [])) = s 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

386 
 tptp_string_for_term format (ATerm (s, ts)) = 
44787  387 
(if s = tptp_empty_list then 
388 
(* used for lists in the optional "source" field of a derivation *) 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

389 
"[" ^ commas (map (tptp_string_for_term format) ts) ^ "]" 
44787  390 
else if is_tptp_equal s then 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

391 
space_implode (" " ^ tptp_equal ^ " ") 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

392 
(map (tptp_string_for_term format) ts) 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

393 
> is_format_higher_order format ? enclose "(" ")" 
44787  394 
else case (s = tptp_ho_forall orelse s = tptp_ho_exists, 
395 
s = tptp_choice andalso is_format_with_choice format, ts) of 

396 
(true, _, [AAbs ((s', ty), tm)]) => 

397 
(* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever 

398 
possible, to work around LEOII 1.2.8 parser limitation. *) 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

399 
tptp_string_for_formula format 
44787  400 
(AQuant (if s = tptp_ho_forall then AForall else AExists, 
401 
[(s', SOME ty)], AAtom tm)) 

402 
 (_, true, [AAbs ((s', ty), tm)]) => 

46320  403 
(* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always 
44787  404 
applied to an abstraction. *) 
405 
tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^ 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

406 
tptp_string_for_term format tm ^ "" 
44787  407 
> enclose "(" ")" 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

408 
 _ => tptp_string_for_app format s (map (tptp_string_for_term format) ts)) 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

409 
 tptp_string_for_term (format as THF _) (AAbs ((s, ty), tm)) = 
44739  410 
"(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^ 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

411 
tptp_string_for_term format tm ^ ")" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

412 
 tptp_string_for_term _ _ = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

413 
raise Fail "unexpected term in firstorder format" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

414 
and tptp_string_for_formula format (AQuant (q, xs, phi)) = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

415 
tptp_string_for_quantifier q ^ 
44739  416 
"[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^ 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

417 
tptp_string_for_formula format phi 
42974
347d5197896e
ensure that the argument of logical negation is enclosed in parentheses in THF mode
blanchet
parents:
42968
diff
changeset

418 
> enclose "(" ")" 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

419 
 tptp_string_for_formula format 
43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

420 
(AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) = 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42967
diff
changeset

421 
space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ") 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

422 
(map (tptp_string_for_term format) ts) 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

423 
> is_format_higher_order format ? enclose "(" ")" 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

424 
 tptp_string_for_formula format (AConn (c, [phi])) = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

425 
tptp_string_for_connective c ^ " " ^ 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

426 
(tptp_string_for_formula format phi 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

427 
> is_format_higher_order format ? enclose "(" ")") 
42974
347d5197896e
ensure that the argument of logical negation is enclosed in parentheses in THF mode
blanchet
parents:
42968
diff
changeset

428 
> enclose "(" ")" 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

429 
 tptp_string_for_formula format (AConn (c, phis)) = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

430 
space_implode (" " ^ tptp_string_for_connective c ^ " ") 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

431 
(map (tptp_string_for_formula format) phis) 
42974
347d5197896e
ensure that the argument of logical negation is enclosed in parentheses in THF mode
blanchet
parents:
42968
diff
changeset

432 
> enclose "(" ")" 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

433 
 tptp_string_for_formula format (AAtom tm) = tptp_string_for_term format tm 
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37931
diff
changeset

434 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

435 
fun tptp_string_for_format CNF = tptp_cnf 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

436 
 tptp_string_for_format CNF_UEQ = tptp_cnf 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

437 
 tptp_string_for_format FOF = tptp_fof 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

438 
 tptp_string_for_format (TFF _) = tptp_tff 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

439 
 tptp_string_for_format (THF _) = tptp_thf 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

440 
 tptp_string_for_format (DFG _) = raise Fail "nonTPTP format" 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

441 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

442 
fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

443 
tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

444 
" : " ^ string_for_type format ty ^ ").\n" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

445 
 tptp_string_for_problem_line format 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

446 
(Formula (ident, kind, phi, source, _)) = 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

447 
tptp_string_for_format format ^ "(" ^ ident ^ ", " ^ 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

448 
tptp_string_for_kind kind ^ ",\n (" ^ 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

449 
tptp_string_for_formula format phi ^ ")" ^ 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

450 
(case source of 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

451 
SOME tm => ", " ^ tptp_string_for_term format tm 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

452 
 NONE => "") ^ ").\n" 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

453 

866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

454 
fun tptp_lines format = 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset

455 
maps (fn (_, []) => [] 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset

456 
 (heading, lines) => 
41491  457 
"\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" :: 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

458 
map (tptp_string_for_problem_line format) lines) 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

459 

866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

460 
fun arity_of_type (AFun (_, ty)) = 1 + arity_of_type ty 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

461 
 arity_of_type _ = 0 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

462 

866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

463 
fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

464 
 binder_atypes _ = [] 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

465 

47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

466 
fun dfg_string_for_formula gen_simp flavor info = 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

467 
let 
46379
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

468 
fun suffix_tag top_level s = 
47041
d810a9130d55
don't generate new SPASS constructs for old SPASS
blanchet
parents:
47038
diff
changeset

469 
if flavor = DFG_Sorted andalso top_level then 
46406  470 
case extract_isabelle_status info of 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

471 
SOME s' => if s' = spec_eqN then s ^ ":lt" 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

472 
else if s' = simpN andalso gen_simp then s ^ ":lr" 
46379
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

473 
else s 
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

474 
 NONE => s 
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

475 
else 
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

476 
s 
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

477 
fun str_for_term top_level (ATerm (s, tms)) = 
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

478 
(if is_tptp_equal s then "equal" > suffix_tag top_level 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

479 
else if s = tptp_true then "true" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

480 
else if s = tptp_false then "false" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

481 
else s) ^ 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

482 
(if null tms then "" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

483 
else "(" ^ commas (map (str_for_term false) tms) ^ ")") 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

484 
 str_for_term _ _ = raise Fail "unexpected term in firstorder format" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

485 
fun str_for_quant AForall = "forall" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

486 
 str_for_quant AExists = "exists" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

487 
fun str_for_conn _ ANot = "not" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

488 
 str_for_conn _ AAnd = "and" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

489 
 str_for_conn _ AOr = "or" 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

490 
 str_for_conn _ AImplies = "implies" 
46379
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

491 
 str_for_conn top_level AIff = "equiv" > suffix_tag top_level 
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

492 
fun str_for_formula top_level (AQuant (q, xs, phi)) = 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

493 
str_for_quant q ^ "(" ^ "[" ^ 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

494 
commas (map (string_for_bound_var (DFG flavor)) xs) ^ "], " ^ 
46379
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

495 
str_for_formula top_level phi ^ ")" 
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

496 
 str_for_formula top_level (AConn (c, phis)) = 
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

497 
str_for_conn top_level c ^ "(" ^ 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

498 
commas (map (str_for_formula false) phis) ^ ")" 
46379
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

499 
 str_for_formula top_level (AAtom tm) = str_for_term top_level tm 
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

500 
in str_for_formula true end 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

501 

47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

502 
fun maybe_enclose bef aft "" = "% " ^ bef ^ aft 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

503 
 maybe_enclose bef aft s = bef ^ s ^ aft 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

504 

2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

505 
fun dfg_lines flavor {is_lpo, gen_weights, gen_prec, gen_simp} ord_info 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

506 
problem = 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

507 
let 
45304
e6901aa86a9e
always use DFG format to talk to SPASS  since that's what we'll need to use anyway to benefit from sorts and other extensions
blanchet
parents:
45303
diff
changeset

508 
val sorted = (flavor = DFG_Sorted) 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

509 
val format = DFG flavor 
46442
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

510 
fun spair (sym, k) = "(" ^ sym ^ ", " ^ string_of_int k ^ ")" 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

511 
fun ary sym = curry spair sym o arity_of_type 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

512 
fun fun_typ sym ty = 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

513 
"function(" ^ sym ^ ", " ^ string_for_type format ty ^ ")." 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

514 
fun pred_typ sym ty = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

515 
"predicate(" ^ 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

516 
commas (sym :: map (string_for_type format) (binder_atypes ty)) ^ ")." 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

517 
fun formula pred (Formula (ident, kind, phi, _, info)) = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

518 
if pred kind then 
47041
d810a9130d55
don't generate new SPASS constructs for old SPASS
blanchet
parents:
47038
diff
changeset

519 
let 
d810a9130d55
don't generate new SPASS constructs for old SPASS
blanchet
parents:
47038
diff
changeset

520 
val rank = 
d810a9130d55
don't generate new SPASS constructs for old SPASS
blanchet
parents:
47038
diff
changeset

521 
if flavor = DFG_Sorted then extract_isabelle_rank info 
d810a9130d55
don't generate new SPASS constructs for old SPASS
blanchet
parents:
47038
diff
changeset

522 
else default_rank 
d810a9130d55
don't generate new SPASS constructs for old SPASS
blanchet
parents:
47038
diff
changeset

523 
in 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

524 
"formula(" ^ dfg_string_for_formula gen_simp flavor info phi ^ 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

525 
", " ^ ident ^ 
46406  526 
(if rank = default_rank then "" else ", " ^ string_of_int rank) ^ 
527 
")." > SOME 

528 
end 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

529 
else 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

530 
NONE 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

531 
 formula _ _ = NONE 
46413  532 
fun filt f = problem > map (map_filter f o snd) > filter_out null 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

533 
val func_aries = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

534 
filt (fn Decl (_, sym, ty) => 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

535 
if is_function_type ty then SOME (ary sym ty) else NONE 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

536 
 _ => NONE) 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

537 
> flat > commas > maybe_enclose "functions [" "]." 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

538 
val pred_aries = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

539 
filt (fn Decl (_, sym, ty) => 
46391
8d8d3c1f1854
really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
blanchet
parents:
46382
diff
changeset

540 
if is_predicate_type ty then SOME (ary sym ty) else NONE 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

541 
 _ => NONE) 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

542 
> flat > commas > maybe_enclose "predicates [" "]." 
45304
e6901aa86a9e
always use DFG format to talk to SPASS  since that's what we'll need to use anyway to benefit from sorts and other extensions
blanchet
parents:
45303
diff
changeset

543 
fun sorts () = 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

544 
filt (fn Decl (_, sym, AType (s, [])) => 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

545 
if s = tptp_type_of_types then SOME sym else NONE 
46413  546 
 _ => NONE) @ [[dfg_individual_type]] 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

547 
> flat > commas > maybe_enclose "sorts [" "]." 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

548 
val ord_info = 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

549 
if sorted andalso (gen_weights orelse gen_prec) then ord_info () else [] 
47030  550 
fun do_term_order_weights () = 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

551 
(if gen_weights then ord_info else []) 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

552 
> map spair > commas > maybe_enclose "weights [" "]." 
46442
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

553 
val syms = 
47030  554 
[func_aries] @ (if sorted then [do_term_order_weights ()] else []) @ 
46442
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

555 
[pred_aries] @ (if sorted then [sorts ()] else []) 
45304
e6901aa86a9e
always use DFG format to talk to SPASS  since that's what we'll need to use anyway to benefit from sorts and other extensions
blanchet
parents:
45303
diff
changeset

556 
fun func_sigs () = 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

557 
filt (fn Decl (_, sym, ty) => 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

558 
if is_function_type ty then SOME (fun_typ sym ty) else NONE 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

559 
 _ => NONE) 
46413  560 
> flat 
45304
e6901aa86a9e
always use DFG format to talk to SPASS  since that's what we'll need to use anyway to benefit from sorts and other extensions
blanchet
parents:
45303
diff
changeset

561 
fun pred_sigs () = 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

562 
filt (fn Decl (_, sym, ty) => 
46391
8d8d3c1f1854
really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
blanchet
parents:
46382
diff
changeset

563 
if is_nontrivial_predicate_type ty then SOME (pred_typ sym ty) 
8d8d3c1f1854
really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
blanchet
parents:
46382
diff
changeset

564 
else NONE 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

565 
 _ => NONE) 
46413  566 
> flat 
45304
e6901aa86a9e
always use DFG format to talk to SPASS  since that's what we'll need to use anyway to benefit from sorts and other extensions
blanchet
parents:
45303
diff
changeset

567 
val decls = if sorted then func_sigs () @ pred_sigs () else [] 
46413  568 
val axioms = 
569 
filt (formula (curry (op <>) Conjecture)) > separate [""] > flat 

570 
val conjs = 

571 
filt (formula (curry (op =) Conjecture)) > separate [""] > flat 

47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

572 
val settings = 
47054  573 
(if is_lpo then ["set_flag(Ordering, 1)."] else []) @ 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

574 
(if gen_prec then 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

575 
[ord_info > map fst > rev > commas 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

576 
> maybe_enclose "set_precedence(" ")."] 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

577 
else 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

578 
[]) 
47053  579 
fun list_of _ [] = [] 
580 
 list_of heading ss = 

581 
"list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @ 

582 
["end_of_list.\n\n"] 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

583 
in 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

584 
"\nbegin_problem(isabelle).\n\n" :: 
47053  585 
list_of "descriptions" 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

586 
["name({**}).", "author({**}).", "status(unknown).", 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

587 
"description({**})."] @ 
47053  588 
list_of "symbols" syms @ 
589 
list_of "declarations" decls @ 

590 
list_of "formulae(axioms)" axioms @ 

591 
list_of "formulae(conjectures)" conjs @ 

592 
list_of "settings(SPASS)" settings @ 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

593 
["end_problem.\n"] 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

594 
end 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

595 

47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

596 
fun lines_for_atp_problem format ord ord_info problem = 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

597 
"% This file was generated by Isabelle (most likely Sledgehammer)\n\ 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

598 
\% " ^ timestamp () ^ "\n" :: 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

599 
(case format of 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

600 
DFG flavor => dfg_lines flavor ord ord_info 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

601 
 _ => tptp_lines format) problem 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset

602 

42939  603 

43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

604 
(** CNF (Metis) and CNF UEQ (Waldmeister) **) 
42939  605 

606 
fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true 

607 
 is_problem_line_negated _ = false 

608 

43193
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

609 
fun is_problem_line_cnf_ueq (Formula (_, _, AAtom (ATerm ((s, _), _)), _, _)) = 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

610 
is_tptp_equal s 
42939  611 
 is_problem_line_cnf_ueq _ = false 
612 

42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42942
diff
changeset

613 
fun open_conjecture_term (ATerm ((s, s'), tms)) = 
43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43422
diff
changeset

614 
ATerm (if is_tptp_variable s then (s > Name.desymbolize false, s') 
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43422
diff
changeset

615 
else (s, s'), tms > map open_conjecture_term) 
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43422
diff
changeset

616 
 open_conjecture_term _ = raise Fail "unexpected higherorder term" 
43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

617 
fun open_formula conj = 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

618 
let 
43193
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

619 
(* We are conveniently assuming that all bound variable names are 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

620 
distinct, which should be the case for the formulas we generate. *) 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

621 
fun opn (pos as SOME true) (AQuant (AForall, _, phi)) = opn pos phi 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

622 
 opn (pos as SOME false) (AQuant (AExists, _, phi)) = opn pos phi 
43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

623 
 opn pos (AConn (ANot, [phi])) = mk_anot (opn (Option.map not pos) phi) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

624 
 opn pos (AConn (c, [phi1, phi2])) = 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

625 
let val (pos1, pos2) = polarities_of_conn pos c in 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

626 
AConn (c, [opn pos1 phi1, opn pos2 phi2]) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

627 
end 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

628 
 opn _ (AAtom t) = AAtom (t > conj ? open_conjecture_term) 
43422
dcbedaf6f80c
added missing case in pattern matching  solves Waldmeister "Match" exceptions that have been plaguing some users
blanchet
parents:
43295
diff
changeset

629 
 opn _ phi = phi 
43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

630 
in opn (SOME (not conj)) end 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42942
diff
changeset

631 
fun open_formula_line (Formula (ident, kind, phi, source, info)) = 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42942
diff
changeset

632 
Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info) 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42942
diff
changeset

633 
 open_formula_line line = line 
42939  634 

635 
fun negate_conjecture_line (Formula (ident, Conjecture, phi, source, info)) = 

42942  636 
Formula (ident, Hypothesis, mk_anot phi, source, info) 
42939  637 
 negate_conjecture_line line = line 
638 

43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

639 
exception CLAUSIFY of unit 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

640 

43126
a7db0afd5200
clausify "<=>" (needed for some type information)
blanchet
parents:
43098
diff
changeset

641 
(* This "clausification" only expands syntactic sugar, such as "phi => psi" to 
a7db0afd5200
clausify "<=>" (needed for some type information)
blanchet
parents:
43098
diff
changeset

642 
"~ phi  psi" and "phi <=> psi" to "~ phi  psi" and "~ psi  phi". We don't 
a7db0afd5200
clausify "<=>" (needed for some type information)
blanchet
parents:
43098
diff
changeset

643 
attempt to distribute conjunctions over disjunctions. *) 
43193
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

644 
fun clausify_formula pos (phi as AAtom _) = [phi > not pos ? mk_anot] 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

645 
 clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

646 
 clausify_formula true (AConn (AOr, [phi1, phi2])) = 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

647 
(phi1, phi2) > pairself (clausify_formula true) 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

648 
> uncurry (map_product (mk_aconn AOr)) 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

649 
 clausify_formula false (AConn (AAnd, [phi1, phi2])) = 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

650 
(phi1, phi2) > pairself (clausify_formula false) 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

651 
> uncurry (map_product (mk_aconn AOr)) 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

652 
 clausify_formula true (AConn (AImplies, [phi1, phi2])) = 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

653 
clausify_formula true (AConn (AOr, [mk_anot phi1, phi2])) 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

654 
 clausify_formula true (AConn (AIff, phis)) = 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

655 
clausify_formula true (AConn (AImplies, phis)) @ 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

656 
clausify_formula true (AConn (AImplies, rev phis)) 
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43163
diff
changeset

657 
 clausify_formula _ _ = raise CLAUSIFY () 
43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

658 

e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

659 
fun clausify_formula_line (Formula (ident, kind, phi, source, info)) = 
43126
a7db0afd5200
clausify "<=>" (needed for some type information)
blanchet
parents:
43098
diff
changeset

660 
let 
a7db0afd5200
clausify "<=>" (needed for some type information)
blanchet
parents:
43098
diff
changeset

661 
val (n, phis) = phi > try (clausify_formula true) > these > `length 
a7db0afd5200
clausify "<=>" (needed for some type information)
blanchet
parents:
43098
diff
changeset

662 
in 
a7db0afd5200
clausify "<=>" (needed for some type information)
blanchet
parents:
43098
diff
changeset

663 
map2 (fn phi => fn j => 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43224
diff
changeset

664 
Formula (ident ^ replicate_string (j  1) "x", kind, phi, source, 
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43224
diff
changeset

665 
info)) 
43126
a7db0afd5200
clausify "<=>" (needed for some type information)
blanchet
parents:
43098
diff
changeset

666 
phis (1 upto n) 
a7db0afd5200
clausify "<=>" (needed for some type information)
blanchet
parents:
43098
diff
changeset

667 
end 
a7db0afd5200
clausify "<=>" (needed for some type information)
blanchet
parents:
43098
diff
changeset

668 
 clausify_formula_line _ = [] 
43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

669 

e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

670 
fun ensure_cnf_problem_line line = 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

671 
line > open_formula_line > negate_conjecture_line > clausify_formula_line 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

672 

e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43092
diff
changeset

673 
fun ensure_cnf_problem problem = 
43126
a7db0afd5200
clausify "<=>" (needed for some type information)
blanchet
parents:
43098
diff
changeset

674 
problem > map (apsnd (maps ensure_cnf_problem_line)) 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43085
diff
changeset

675 

42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

676 
fun filter_cnf_ueq_problem problem = 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

677 
problem 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

678 
> map (apsnd (map open_formula_line 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

679 
#> filter is_problem_line_cnf_ueq 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

680 
#> map negate_conjecture_line)) 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

681 
> (fn problem => 
42939  682 
let 
43824
0234156d3fbe
don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes
blanchet
parents:
43692
diff
changeset

683 
val lines = problem > maps snd 
0234156d3fbe
don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes
blanchet
parents:
43692
diff
changeset

684 
val conjs = lines > filter is_problem_line_negated 
0234156d3fbe
don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes
blanchet
parents:
43692
diff
changeset

685 
in if length conjs = 1 andalso conjs <> lines then problem else [] end) 
38017
3ad3e3ca2451
move Sledgehammerspecific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38014
diff
changeset

686 

37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset

687 

42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

688 
(** Symbol declarations **) 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

689 

1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

690 
fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

691 
 add_declared_syms_in_problem_line _ = I 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

692 
fun declared_syms_in_problem problem = 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

693 
fold (fold add_declared_syms_in_problem_line o snd) problem [] 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

694 

37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset

695 
(** Nice names **) 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37642
diff
changeset

696 

37624  697 
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs 
698 
fun pool_map f xs = 

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

700 

42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
41769
diff
changeset

701 
val no_qualifiers = 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
41769
diff
changeset

702 
let 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
41769
diff
changeset

703 
fun skip [] = [] 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
41769
diff
changeset

704 
 skip (#"." :: cs) = skip cs 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
41769
diff
changeset

705 
 skip (c :: cs) = if Char.isAlphaNum c then skip cs else c :: keep cs 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
41769
diff
changeset

706 
and keep [] = [] 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
41769
diff
changeset

707 
 keep (#"." :: cs) = skip cs 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
41769
diff
changeset

708 
 keep (c :: cs) = c :: keep cs 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
41769
diff
changeset

709 
in String.explode #> rev #> keep #> rev #> String.implode end 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
41769
diff
changeset

710 

42761
8ea9c6fa8b53
fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP
blanchet
parents:
42752
diff
changeset

711 
(* Long names can slow down the ATPs. *) 
42724
4d6bcf846759
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents:
42722
diff
changeset

712 
val max_readable_name_size = 20 
42567
d012947edd36
shorten readable names  they can get really long with monomorphization, which actually slows down the ATPs
blanchet
parents:
42543
diff
changeset

713 

43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

714 
(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

715 
unreadable "op_1", "op_2", etc., in the problem files. "eq" is reserved to 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

716 
ensure that "HOL.eq" is correctly mapped to equality (not clear whether this 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

717 
is still necessary). *) 
45939
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

718 
val reserved_nice_names = [tptp_old_equal, "op", "eq"] 
42939  719 

46414
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

720 
(* hack to get the same hashing across Mirabelle runs (see "mirabelle.pl") *) 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

721 
fun cleanup_mirabelle_name s = 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

722 
let 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

723 
val mirabelle_infix = "_Mirabelle_" 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

724 
val random_suffix_len = 10 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

725 
val (s1, s2) = Substring.position mirabelle_infix (Substring.full s) 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

726 
in 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

727 
if Substring.isEmpty s2 then 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

728 
s 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

729 
else 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

730 
Substring.string s1 ^ 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

731 
Substring.string (Substring.triml (size mirabelle_infix + random_suffix_len) s2) 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

732 
end 
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

733 

46378  734 
fun readable_name protect full_name s = 
45939
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

735 
(if s = full_name then 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

736 
s 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

737 
else 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

738 
s > no_qualifiers 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

739 
> perhaps (try (unprefix "'")) 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

740 
> Name.desymbolize (Char.isUpper (String.sub (full_name, 0))) 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

741 
> (fn s => 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

742 
if size s > max_readable_name_size then 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

743 
String.substring (s, 0, max_readable_name_size div 2  4) ^ 
46414
4ed12518fb81
improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents:
46413
diff
changeset

744 
string_of_int (hash_string (cleanup_mirabelle_name full_name)) ^ 
45939
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

745 
String.extract (s, size s  max_readable_name_size div 2 + 4, 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

746 
NONE) 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

747 
else 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

748 
s) 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

749 
> (fn s => 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

750 
if member (op =) reserved_nice_names s then full_name else s)) 
46378  751 
> protect 
37624  752 

45939
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

753 
fun nice_name _ (full_name, _) NONE = (full_name, NONE) 
46378  754 
 nice_name protect (full_name, desired_name) (SOME the_pool) = 
42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

755 
if is_built_in_tptp_symbol full_name then 
39384  756 
(full_name, SOME the_pool) 
757 
else case Symtab.lookup (fst the_pool) full_name of 

37624  758 
SOME nice_name => (nice_name, SOME the_pool) 
759 
 NONE => 

760 
let 

46378  761 
val nice_prefix = readable_name protect full_name desired_name 
37624  762 
fun add j = 
763 
let 

42644  764 
val nice_name = 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

765 
nice_prefix ^ (if j = 1 then "" else string_of_int j) 
37624  766 
in 
767 
case Symtab.lookup (snd the_pool) nice_name of 

768 
SOME full_name' => 

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

770 
else add (j + 1) 

771 
 NONE => 

772 
(nice_name, 

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

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

775 
end 

47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47030
diff
changeset

776 
in add 1 > apsnd SOME end 
37624  777 

46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46445
diff
changeset

778 
fun avoid_clash_with_alt_ergo_type_vars s = 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46445
diff
changeset

779 
if is_tptp_variable s then s else s ^ "_" 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46445
diff
changeset

780 

46378  781 
fun avoid_clash_with_dfg_keywords s = 
782 
let val n = String.size s in 

46443
c86276014571
improved KBO weights  beware of explicit applications
blanchet
parents:
46442
diff
changeset

783 
if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse 
c86276014571
improved KBO weights  beware of explicit applications
blanchet
parents:
46442
diff
changeset

784 
String.isSubstring "_" s then 
46378  785 
s 
786 
else 

787 
String.substring (s, 0, n  1) ^ 

788 
String.str (Char.toUpper (String.sub (s, n  1))) 

789 
end 

790 

45939
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

791 
fun nice_atp_problem readable_names format problem = 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

792 
let 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

793 
val empty_pool = 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

794 
if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE 
46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46445
diff
changeset

795 
val avoid_clash = 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46445
diff
changeset

796 
case format of 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46445
diff
changeset

797 
TFF (TPTP_Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46445
diff
changeset

798 
 DFG _ => avoid_clash_with_dfg_keywords 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46445
diff
changeset

799 
 _ => I 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46445
diff
changeset

800 
val nice_name = nice_name avoid_clash 
45939
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

801 
fun nice_type (AType (name, tys)) = 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

802 
nice_name name ##>> pool_map nice_type tys #>> AType 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

803 
 nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

804 
 nice_type (ATyAbs (names, ty)) = 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

805 
pool_map nice_name names ##>> nice_type ty #>> ATyAbs 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

806 
fun nice_term (ATerm (name, ts)) = 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

807 
nice_name name ##>> pool_map nice_term ts #>> ATerm 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

808 
 nice_term (AAbs ((name, ty), tm)) = 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

809 
nice_name name ##>> nice_type ty ##>> nice_term tm #>> AAbs 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

810 
fun nice_formula (AQuant (q, xs, phi)) = 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

811 
pool_map nice_name (map fst xs) 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

812 
##>> pool_map (fn NONE => pair NONE 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

813 
 SOME ty => nice_type ty #>> SOME) (map snd xs) 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

814 
##>> nice_formula phi 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

815 
#>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi)) 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

816 
 nice_formula (AConn (c, phis)) = 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

817 
pool_map nice_formula phis #>> curry AConn c 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

818 
 nice_formula (AAtom tm) = nice_term tm #>> AAtom 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

819 
fun nice_problem_line (Decl (ident, sym, ty)) = 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

820 
nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Decl (ident, sym, ty)) 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

821 
 nice_problem_line (Formula (ident, kind, phi, source, info)) = 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

822 
nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info)) 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

823 
fun nice_problem problem = 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

824 
pool_map (fn (heading, lines) => 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

825 
pool_map nice_problem_line lines #>> pair heading) problem 
711fec5b4f61
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents:
45938
diff
changeset

826 
in nice_problem problem empty_pool end 
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset

827 

f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff
changeset

828 
end; 