author  blanchet 
Thu, 09 Feb 2012 14:42:18 +0100  
changeset 46445  ef9d534e9119 
parent 46443  c86276014571 
child 46643  a88bccd2b567 
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 

44754  25 
datatype tptp_polymorphism = TPTP_Monomorphic  TPTP_Polymorphic 
26 
datatype tptp_explicitness = TPTP_Implicit  TPTP_Explicit 

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

27 
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

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

29 

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

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

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

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

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

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

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

37 

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

38 
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

39 
datatype 'a problem_line = 
42963  40 
Decl of string * 'a * 'a ho_type  
44402  41 
Formula of string * formula_kind 
42 
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula 

43 
* (string, string ho_type) ho_term option 

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

45 
type 'a problem = (string * 'a problem_line list) list 
37992  46 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

76 
val tptp_empty_list : string 
46406  77 
val isabelle_info_prefix : string 
78 
val isabelle_info : atp_format > string > int > (string, 'a) ho_term list 

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

79 
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

80 
val extract_isabelle_rank : (string, 'a) ho_term list > int 
46406  81 
val introN : string 
82 
val elimN : string 

83 
val simpN : string 

84 
val spec_eqN : string 

85 
val rankN : string 

86 
val minimum_rank : int 

87 
val default_rank : int 

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

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

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

90 
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

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

92 
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

93 
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

94 
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

95 
val individual_atype : (string * string) ho_type 
42942  96 
val mk_anot : ('a, 'b, 'c) formula > ('a, 'b, 'c) formula 
97 
val mk_aconn : 

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

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

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

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

101 
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

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

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

104 
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

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

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

107 
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

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

109 
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

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

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

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

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

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

115 
atp_format > (unit > (string * int) list) > string problem > string list 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43085
diff
changeset

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

117 
(string * string) problem > (string * string) problem 
42939  118 
val filter_cnf_ueq_problem : 
119 
(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

120 
val declared_syms_in_problem : (string * ''a) problem > (string * ''a) list 
39452  121 
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

122 
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

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

124 
* (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

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

126 

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

127 
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

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

129 

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

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

131 

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

132 

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

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

134 

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

135 
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

136 
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

137 
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

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

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

141 
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

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

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

144 

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

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

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

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

148 
ATyAbs of 'a list * 'a ho_type 
42963  149 

44754  150 
datatype tptp_polymorphism = TPTP_Monomorphic  TPTP_Polymorphic 
151 
datatype tptp_explicitness = TPTP_Implicit  TPTP_Explicit 

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

152 
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

153 
datatype dfg_flavor = DFG_Unsorted  DFG_Sorted 
44499  154 

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

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

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

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

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

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

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

162 

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

163 
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

164 
datatype 'a problem_line = 
42963  165 
Decl of string * 'a * 'a ho_type  
46406  166 
Formula of string * formula_kind 
167 
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula 

168 
* (string, string ho_type) ho_term option 

169 
* (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

170 
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

171 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

202 
val tptp_empty_list = "[]" 
42722  203 

46406  204 
val isabelle_info_prefix = "isabelle_" 
205 

206 
val introN = "intro" 

207 
val elimN = "elim" 

208 
val simpN = "simp" 

209 
val spec_eqN = "spec_eq" 

210 
val rankN = "rank" 

211 

212 
val minimum_rank = 0 

213 
val default_rank = 1000 

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

214 
val default_kbo_weight = 1 
46406  215 

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

217 
process Isabelle metainformation. *) 

218 
fun isabelle_info (DFG DFG_Sorted) status rank = 

219 
[] > rank <> default_rank 

220 
? cons (ATerm (isabelle_info_prefix ^ rankN, 

221 
[ATerm (string_of_int rank, [])])) 

222 
> status <> "" ? cons (ATerm (isabelle_info_prefix ^ status, [])) 

223 
 isabelle_info _ _ _ = [] 

224 

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

226 
try (unprefix isabelle_info_prefix) s 

227 
 extract_isabelle_status _ = NONE 

228 

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

230 
(case List.last tms of 

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

232 
 _ => default_rank) 

233 
 extract_isabelle_rank _ = default_rank 

234 

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

235 
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

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

237 
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

238 
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

239 
val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol) 
42939  240 

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

241 
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

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

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

244 

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

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

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

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

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

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

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

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

252 
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

253 

42942  254 
fun mk_anot (AConn (ANot, [phi])) = phi 
255 
 mk_anot phi = AConn (ANot, [phi]) 

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

257 

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

258 
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

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

260 
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

261 
 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

262 
 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

263 
 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

264 

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

265 
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

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

267 
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

268 
 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

269 
 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

270 
 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

271 

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

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

273 
let 
44501  274 
fun fld pos (AQuant (_, _, phi)) = fld pos phi 
275 
 fld pos (AConn conn) = aconn_fold pos fld conn 

276 
 fld pos (AAtom tm) = f pos tm 

277 
in fld pos end 

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

278 

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

279 
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

280 
 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

281 
 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

282 

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

283 
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

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

285 
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

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

287 
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

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

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

290 
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

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

292 

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

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

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

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

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

299 

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

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

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

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

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

304 
 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

305 

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

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

307 
if is_format_higher_order format then 
44787  308 
"(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")" 
309 
else 

310 
func ^ "(" ^ commas args ^ ")" 

311 

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

312 
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

313 
 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

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

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

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

317 
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

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

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

320 
 flatten_type _ = 
42963  321 
raise Fail "unexpected higherorder type in firstorder format" 
322 

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

324 

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

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

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

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

329 
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

330 
 str _ (AType (s, tys)) = 
44787  331 
let val ss = tys > map (str false) in 
332 
if s = tptp_product_type then 

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

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

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

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

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

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

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

341 
(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

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

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

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

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

348 

44787  349 
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

350 
 string_for_type format ty = str_for_type format (flatten_type ty) 
42963  351 

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

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

353 
 tptp_string_for_quantifier AExists = tptp_exists 
42963  354 

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

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

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

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

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

359 
 tptp_string_for_connective AIff = tptp_iff 
42963  360 

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

361 
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

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

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

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

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

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

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

368 
"") 
42963  369 

44754  370 
fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true 
371 
 is_format_with_choice _ = false 

372 

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

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

374 
 tptp_string_for_term format (ATerm (s, ts)) = 
44787  375 
(if s = tptp_empty_list then 
376 
(* 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

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

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

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

381 
> is_format_higher_order format ? enclose "(" ")" 
44787  382 
else case (s = tptp_ho_forall orelse s = tptp_ho_exists, 
383 
s = tptp_choice andalso is_format_with_choice format, ts) of 

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

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

386 
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

387 
tptp_string_for_formula format 
44787  388 
(AQuant (if s = tptp_ho_forall then AForall else AExists, 
389 
[(s', SOME ty)], AAtom tm)) 

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

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

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

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

396 
 _ => 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

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

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

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

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

402 
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

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

405 
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

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

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

408 
(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

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

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

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

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

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

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

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

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

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

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

419 
(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

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

421 
 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

422 

43692  423 
fun the_source (SOME source) = source 
424 
 the_source NONE = 

425 
ATerm ("inference", 

426 
ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", []))) 

42639  427 

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

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

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

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

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

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

433 
 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

434 

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

435 
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

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

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

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

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

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

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

442 
tptp_string_for_formula format phi ^ ")" ^ 
42939  443 
(case (source, info) of 
46406  444 
(NONE, []) => "" 
445 
 (SOME tm, []) => ", " ^ tptp_string_for_term format tm 

446 
 (_, tms) => 

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

447 
", " ^ tptp_string_for_term format (the_source source) ^ 
46406  448 
", " ^ tptp_string_for_term format (ATerm (tptp_empty_list, tms))) ^ 
449 
").\n" 

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

450 

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

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

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

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

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

456 

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

457 
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

458 
 arity_of_type _ = 0 
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 binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

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

462 

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

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

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

465 
fun suffix_tag top_level s = 
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

466 
if top_level then 
46406  467 
case extract_isabelle_status info of 
46379
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

468 
SOME s' => if s' = simpN then s ^ ":lr" 
46393  469 
else if s' = spec_eqN then s ^ ":lt" 
46379
de5dd84717c1
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents:
46378
diff
changeset

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

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

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

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

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

475 
(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

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

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

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

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

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

481 
 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

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

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

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

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

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

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

488 
 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

489 
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

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

491 
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

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

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

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

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

496 
 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

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

498 

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

499 
fun dfg_lines flavor kbo_weights problem = 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

500 
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

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

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

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

504 
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

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

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

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

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

509 
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

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

511 
if pred kind then 
46406  512 
let val rank = extract_isabelle_rank info in 
513 
"formula(" ^ dfg_string_for_formula flavor info phi ^ ", " ^ ident ^ 

514 
(if rank = default_rank then "" else ", " ^ string_of_int rank) ^ 

515 
")." > SOME 

516 
end 

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

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

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

519 
 formula _ _ = NONE 
46413  520 
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

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

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

523 
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

524 
 _ => NONE) 
46413  525 
> flat > commas > enclose "functions [" "]." 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

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

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

528 
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

529 
 _ => NONE) 
46413  530 
> flat > commas > 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

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

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

533 
if s = tptp_type_of_types then SOME sym else NONE 
46413  534 
 _ => NONE) @ [[dfg_individual_type]] 
535 
> flat > commas > enclose "sorts [" "]." 

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

536 
fun do_kbo_weights () = 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

537 
kbo_weights () > map spair > commas > enclose "weights [" "]." 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

538 
val syms = 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

539 
[func_aries] @ (if sorted then [do_kbo_weights ()] else []) @ 
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46414
diff
changeset

540 
[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

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

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

543 
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

544 
 _ => NONE) 
46413  545 
> 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

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

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

548 
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

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

550 
 _ => NONE) 
46413  551 
> 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

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

555 
val conjs = 

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

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

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

558 
 list_of heading ss = 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

559 
"list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @ 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

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

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

562 
"\nbegin_problem(isabelle).\n\n" :: 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

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

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

565 
"description({**})."] @ 
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

566 
list_of "symbols" syms @ 
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 
list_of "declarations" decls @ 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

568 
list_of "formulae(axioms)" axioms @ 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

569 
list_of "formulae(conjectures)" conjs @ 
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
44787
diff
changeset

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

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

572 

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

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

574 
"% 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

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

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

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

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

579 

42939  580 

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

581 
(** CNF (Metis) and CNF UEQ (Waldmeister) **) 
42939  582 

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

584 
 is_problem_line_negated _ = false 

585 

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

586 
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

587 
is_tptp_equal s 
42939  588 
 is_problem_line_cnf_ueq _ = false 
589 

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

590 
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

591 
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

592 
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

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

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

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

596 
(* 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

597 
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

598 
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

599 
 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

600 
 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

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

602 
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

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

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

605 
 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

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

607 
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

608 
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

609 
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

610 
 open_formula_line line = line 
42939  611 

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

42942  613 
Formula (ident, Hypothesis, mk_anot phi, source, info) 
42939  614 
 negate_conjecture_line line = line 
615 

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

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

617 

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

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

619 
"~ 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

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

621 
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

622 
 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

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

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

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

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

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

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

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

630 
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

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

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

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

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

635 

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

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

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

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

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

640 
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

641 
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

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

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

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

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

646 

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

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

648 
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

649 

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

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

651 
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

652 

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

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

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

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

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

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

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

660 
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

661 
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

662 
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

663 

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

664 

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

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

666 

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

667 
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

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

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

670 
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

671 

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

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

673 

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

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

677 

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

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

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

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

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

682 
 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

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

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

685 
 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

686 
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

687 

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

688 
(* 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

689 
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

690 

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

691 
(* "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

692 
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

693 
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

694 
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

695 
val reserved_nice_names = [tptp_old_equal, "op", "eq"] 
42939  696 

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

697 
(* 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

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

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

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

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

702 
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

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

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

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

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

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

708 
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

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

710 

46378  711 
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

712 
(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

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

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

715 
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

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

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

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

719 
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

720 
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

721 
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

722 
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

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

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

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

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

727 
if member (op =) reserved_nice_names s then full_name else s)) 
46378  728 
> protect 
37624  729 

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

730 
fun nice_name _ (full_name, _) NONE = (full_name, NONE) 
46378  731 
 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

732 
if is_built_in_tptp_symbol full_name then 
39384  733 
(full_name, SOME the_pool) 
734 
else case Symtab.lookup (fst the_pool) full_name of 

37624  735 
SOME nice_name => (nice_name, SOME the_pool) 
736 
 NONE => 

737 
let 

46378  738 
val nice_prefix = readable_name protect full_name desired_name 
37624  739 
fun add j = 
740 
let 

42644  741 
val nice_name = 
44407  742 
nice_prefix ^ (if j = 0 then "" else string_of_int j) 
37624  743 
in 
744 
case Symtab.lookup (snd the_pool) nice_name of 

745 
SOME full_name' => 

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

747 
else add (j + 1) 

748 
 NONE => 

749 
(nice_name, 

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

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

752 
end 

753 
in add 0 > apsnd SOME end 

754 

46378  755 
fun avoid_clash_with_dfg_keywords s = 
756 
let val n = String.size s in 

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

757 
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

758 
String.isSubstring "_" s then 
46378  759 
s 
760 
else 

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

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

763 
end 

764 

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

765 
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

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

767 
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

768 
if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE 
46378  769 
val nice_name = 
770 
nice_name (case format of DFG _ => avoid_clash_with_dfg_keywords  _ => I) 

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

771 
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

772 
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

773 
 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

774 
 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

775 
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

776 
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

777 
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

778 
 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

779 
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

780 
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

781 
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

782 
##>> 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

783 
 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

784 
##>> 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

785 
#>> (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

786 
 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

787 
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

788 
 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

789 
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

790 
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

791 
 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

792 
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

793 
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

794 
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

795 
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

796 
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

797 

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

798 
end; 